[Colloq] Thesis Defense - Vasileios Koutavas - Tuesday, Sept. 16

[Rachel Kalweit]

Vassilis Koutavas will being doing his Thesis Defense on Tuesday, Sept. 16 in room 366 at 11:45am.

Title: Reasoning about Imperative and Higher-Order Programs

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.

Committee Members:
Mitchell Wand (advisor)
Matthias Felleisen
Riccardo Puccela
Radha Jagadeesan (external)