2015 | OriginalPaper | Buchkapitel
Logical Relations and Nondeterminism
verfasst von : Martin Hofmann
Erschienen in: Software, Services, and Systems
Verlag: Springer International Publishing
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
The purpose of this article is to illustrate some technical difficulties encountered when trying to extend a logical relation to the Hoare powerdomain. We give a partial solution and some applications. Our vehicle is a simple call-by-value programming language with binary nondeterministic choice. We define both a big-step operational semantics and a denotational semantics using the Hoare powerdomain. Using our logical relation we then show equivalence of the two semantics in the sense of computational adequacy and some type-dependent program equivalences.