Document Type
Article
Date
1995
Keywords
PCF, Kripke logic relations, logic relations
Language
English
Disciplines
Computer Sciences
Description/Abstract
Sieber has described a model of PCF consisting of continuous functions that are invariant under certain (finitary) logical relations, and shown that it is fully abstract for closed terms of up to third-order types. We show that one may achieve full abstraction at all types using a form of "Kripke logical relations" introduced by Jung and Tiuryn to characterize λ definability.
Recommended Citation
O'Hearn, Peter W. and Riecke, John G., "Kripke Logical Relations and PCF" (1995). College of Engineering and Computer Science - Former Departments, Centers, Institutes and Projects. 3.
https://surface.syr.edu/lcsmith_other/3
Creative Commons License
This work is licensed under a Creative Commons Attribution 3.0 License.
