Lax Logical Relations

Gordon D. Plotkin, John Power, Donald Sannella, Robert D. Tennent

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.
Original languageEnglish
Title of host publicationAutomata, Languages and Programming
Subtitle of host publication27th International Colloquium, ICALP 2000, Geneva, Switzerland, July 9-15, 2000, Proceedings
PublisherSpringer Berlin Heidelberg
Pages85-102
Number of pages18
ISBN (Electronic)978-3-540-45022-1
ISBN (Print)978-3-540-67715-4
DOIs
Publication statusPublished - 2000

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume1853
ISSN (Print)0302-9743

Fingerprint Dive into the research topics of 'Lax Logical Relations'. Together they form a unique fingerprint.

Cite this