Lax Logical Relations
Plotkin, G., Power, J., Sannella, D. and Tennent, R., 2002. Lax Logical Relations. In: Automata, Languages and Programming: 27th International Colloquium, ICALP 2000 Geneva, Switzerland, July 9–15, 2000 Proceedings. Vol. 1853. , pp. 85-102. (Lecture Notes in Computer Science)
Related documents:This repository does not currently have the full-text of this item.
You may be able to access a copy if URLs are provided below.
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.
|Item Type||Book Sections|
|Creators||Plotkin, G., Power, J., Sannella, D. and Tennent, R.|
|Departments||Faculty of Science > Computer Science|
Actions (login required)