Edinburgh Research Archive

Lax Logical Relations

Simple item page
dc.contributor.author
Plotkin, Gordon
en
dc.contributor.author
Power, John
en
dc.contributor.author
Sannella, Donald
en
dc.contributor.author
Tennent, Robert
en
dc.coverage.spatial
17
en
dc.date.accessioned
2003-11-06T11:06:43Z
dc.date.available
2003-11-06T11:06:43Z
dc.date.issued
2000
dc.description.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.
en
dc.format.extent
525147 bytes
en
dc.format.mimetype
application/pdf
en
dc.identifier.citation
AUTOMATA LANGUAGES AND PROGRAMMING LECTURE NOTES IN COMPUTER SCIENCE 1853: 85-102 2000
dc.identifier.issn
0302-9743
dc.identifier.uri
http://hdl.handle.net/1842/223
dc.language.iso
en
dc.publisher
SPRINGER-VERLAG
en
dc.subject
Laboratory for Foundations of Computer Science
en
dc.title
Lax Logical Relations
en
dc.type
Preprint
en

Files

Original bundle

Now showing 1 - 1 of 1
Name:
laxlr.pdf
Size:
512.84 KB
Format:
Adobe Portable Document Format
Download

This item appears in the following Collection(s)

Informatics Publications