[isabelle] New AFP entry: Logical Relations for PCF

Logical Relations for PCF
Peter Gammie

We apply Andy Pitts's methods of defining relations over domains to several
classical results in the literature. We show that the Y combinator coincides
with the domain-theoretic fixpoint operator, that parallel-or and the Plotkin
existential are not definable in PCF, that the continuation semantics for PCF
coincides with the direct semantics, and that our domain-theoretic semantics for
PCF is adequate for reasoning about contextual equivalence in an operational
semantics. Our version of PCF is untyped and has both strict and non-strict
function abstractions. The development is carried out in HOLCF.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.