Lax Logical Relations

Reference:

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:

Official URL:

http://dx.doi.org/10.1007/3-540-45022-X_9

Abstract

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.

Export

Actions (login required)