Logical relations and nondeterminism

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 callby- 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.