Advisor(s)

Mitchell Wand

Contributor(s)

Matthias Felleisen, Riccardo Pucella, Radha Jagadeesan

Date of Award

2008

Date Accepted

9-2008

Degree Grantor

Northeastern University

Degree Level

Ph.D.

Degree Name

Doctor of Philosophy

Department or Academic Unit

College of Computer and Information Science.

Keywords

Computer science, Programming languages, Equivalence, Proof technique

Subject Categories

Computer programs--Correctness, Logic

Disciplines

Computer Sciences

Abstract

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.

Document Type

Dissertation

Rights Holder

Vasileios Koutavas


View Full Text

Click button above to open, or right-click to save.

Share

COinS