Logical relations and nondeterminism
M Hofmann - Software, Services, and Systems: Essays Dedicated to …, 2015 - Springer
M Hofmann
Software, Services, and Systems: Essays Dedicated to Martin Wirsing on the …, 2015•SpringerThe 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 …
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 …
Abstract
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.
Springer