TY - CHAP
T1 - Lax Logical Relations
AU - Plotkin, Gordon
AU - Power, John
AU - Sannella, Donald
AU - Tennent, Robert
PY - 2002
Y1 - 2002
N2 - 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.
AB - 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.
UR - http://dx.doi.org/10.1007/3-540-45022-X_9
U2 - 10.1007/3-540-45022-X_9
DO - 10.1007/3-540-45022-X_9
M3 - Chapter or section
VL - 1853
T3 - Lecture Notes in Computer Science
SP - 85
EP - 102
BT - Automata, Languages and Programming: 27th International Colloquium, ICALP 2000 Geneva, Switzerland, July 9–15, 2000 Proceedings
ER -