Email Gateway (Aug 19 2022 at 07:49): Email Gateway (Aug 19 2022 at 07:49):From: Tobias Nipkow <nipkow@in.tum.de>
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.
http://afp.sourceforge.net/entries/PCF.shtml
Enjoy!
Last updated: Apr 20 2024 at 01:05 UTC