Matthias Felleisen, Riccardo Pucella, Radha Jagadeesan
Date of Award
Doctor of Philosophy
Department or Academic Unit
College of Computer and Information Science.
Computer science, Programming languages, Equivalence, Proof technique
Computer programs--Correctness, Logic
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.
Koutavas, Vasileios, "Reasoning about imperative and higher-order programs" (2008). Computer Science Dissertations. Paper 6. http://hdl.handle.net/2047/d10016545
Click button above to open, or right-click to save.