Reasoning about imperative and higher-order programs

• Online Access: http://hdl.handle.net/2047/d10016545

Contextual equivalence, namely the property that two expressions are indistinguishable inside any program context, is a fundamental property of program expressions. Discovering methods that enable formal reasoning about contextual equivalence is hard and highly dependent on the features of the programming language. In this dissertation we present a technique for systematically deriving reasoning methods for contextual equivalence, which are sound and complete in a variety of languages, but also useful for proving many equivalences. The advantages of the derived reasoning methods are that they successfully deal with imperative as well as higher-order features. We demonstrate our technique by deriving sound and complete methods for proving contextual equivalence in the call-by-value lambda calculus, a lambda calculus with higher-order store, the nu-calculus, an imperative object calculus, and an imperative core of Java.