Lax Logical Relations

Lax logical relations are a categorical generalisation of logical relations; though they preserve product types, they need not preserve exponential types. But, like logical relations, they are preserved by the meanings of all lambda-calculus terms. We show that lax logical relations coincide with the correspondences of Schoett, the algebraic relations of Mitchell and the pre-logical relations of Honsell and Sannella on Henkin models, but also generalise naturally to models in cartesian closed categories and to richer languages.

• Type: Conference
• Year: 2000
• Where: ICALP
• Authors: Gordon D. Plotkin, John Power, Donald Sannella, Robert D. Tennent
• Keywords: Algebraic Relations, ICALP 2000, Lax Logical Relations, Logical Relations, Programming Languages