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. © 1995 Academic Press, Inc.
Cite
CITATION STYLE
APA
Ohearn, P. W., & Riecke, J. G. (1995). Kripke logical relations and PCF. Information and Computation, 120(1), 107–116. https://doi.org/10.1006/inco.1995.1103
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
Already have an account? Sign in
Sign up for free