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 abstractionlogic for computable functionsKripke logical relations

Mathematics Subject Classification ID

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

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

(21)

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

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)