Sciweavers

Share
ICALP
2000
Springer

Lax Logical Relations

10 years 3 months ago
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.
Gordon D. Plotkin, John Power, Donald Sannella, Ro
Added 24 Aug 2010
Updated 24 Aug 2010
Type Conference
Year 2000
Where ICALP
Authors Gordon D. Plotkin, John Power, Donald Sannella, Robert D. Tennent
Comments (0)
books