Kripke logical relations and PCF

DOI10.1006/INCO.1995.1103MaRDI QIDQ1898483zbMATH OpenOpenAlexWikidataFDO

Authors Peter W. O'Hearn, Jon G. Riecke

Publication date 11 May 1999

Published in Information and Computation (Search for Journal in Brave)

Copyright license Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International

Full work available at URL https://surface.syr.edu/cgi/viewcontent.cgi?article=1002&context=lcsmith_other

zbMATH Keywords

full abstractionKripke logical relationslogic for computable functions

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Categorical logic, topoi (03G30) Semantics in the theory of computing (68Q55)

Review text

\textit{A. Jung} and \textit{J. Tiuryn} [Lect. Notes Comput. Sci. 664, 245-257 (1993; Zbl 0795.03021)] introduced ``Kripke logical relations to characterize \(\lambda\)-definability. Here, these relations are used to show that \textit{K. Sieber's} model of PCF [``New steps toward full abstraction for local variables, in: ACM SIGLPLAN Workshop on State in Programming Languages, 88-100 (1993)], consisting of continuous functions that are invariant under certain (finitary) logical relations, is fully abstract at all types.

Recommendations

• scientific article; zbMATH DE number 431771
• Inductive Definition and Domain Theoretic Properties of Fully Abstract
• scientific article; zbMATH DE number 1523049
• Full abstraction for PCF
• scientific article; zbMATH DE number 3902022

Cited in

(23)

• Full abstraction for the second order subset of an Algol-like language
• Relative definability of boolean functions via hypergraphs
• The sequentially realizable functionals
• Games and full abstraction for FPC.
• Full abstraction for PCF
• Prelogical relations
• Game-theoretic analysis of call-by-value computation
• On phase semantics and denotational semantics in multiplicative-additive linear logic
• Cryptographic logical relations
• A stable programming language
• A relational account of call-by-value sequentiality
• Definability and full abstraction
• scientific article; zbMATH DE number 177255 (Why is no real title available?)
• Program equivalence in a simple language with state
• scientific article; zbMATH DE number 2170850 (Why is no real title available?)
• Full abstraction for non-deterministic and probabilistic extensions of PCF. I: The angelic cases
• On phase semantics and denotational semantics: The exponentials
• Finitary PCF is not decidable
• Logical predicates in higher-order mathematical operational semantics
• Concrete categories and higher-order recursion. With applications including probability, differentiability, and full abstraction
• A characterization of lambda definability in categorical models of implicit polymorphism
• Fully abstract normal form bisimulation for call-by-value PCF
• Bialgebraic reasoning on higher-order program equivalence

This page was built for publication: Kripke logical relations and PCF

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1898483)