Research

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:

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.

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.

Details

Item Type Book Sections
CreatorsPlotkin, G., Power, J., Sannella, D. and Tennent, R.
DOI10.1007/3-540-45022-X_9
DepartmentsFaculty of Science > Computer Science
StatusPublished
ID Code26474

Export

Actions (login required)

View Item