Semantics of Programming Languages

Bisimulations and Contextual Equivalence

We are currently exploring the use of bisimulations to prove the contextual equivalence of untyped, higher-order imperative programs. We have developed a new notion of bisimulation that leads to smaller and more tractable relations than previous methods. It also handles examples with higher-order procedures, which pose difficulties for existing methods. We have a paper on this at POPL 2006.

The bisimulation conditions are derived by manually extracting proof obligations from a hypothetical direct proof of contextual equivalence. This suggests a method for deriving definitions of bisimulation for other languages. We illustrate this technique for the imperative object calculus in a paper to appear at ESOP 2006.

Monads and Operational Semantics

We look at monads every so often. We had a paper on this subject in ICFP 2004. There we use monads to formalize the two basic models of backtracking: the stream model and the two-continuation model. We relate the two models using logical relations. We accommodate higher-order values and infinite computations. We also provide an operational semantics, and we prove it adequate for both models.

We've also completed a short paper about the Krivine Machine; this has to do with operational semantics, though not (so far) about monads.

Aspect-Oriented Programming

Aspect-oriented programming (AOP) is a promising recent technology for allowing adaptation of program units across module boundaries. We have developed a semantics for advice and dynamic join points in a subset of AspectJ. We would like to extend this model to cover more features, and also to abstract it to make it more amendable to mathematical analysis. We are interested in reconciling AOP with traditional notions of program modularity, and in developing program analyses for aspect-oriented programming languages. We gave an invited talk at ICFP 2003 on this subject. (Other AOP-related papers)

Analysis-Based Program Transformation

We spent most of the 1990's working on understanding just how a program analysis justifies the program transformation that is typically based upon it. We studied a sequence of analysis-based transformations, including offline partial evaluation, lightweight closure conversion, useless variable elimination, and destructive update introduction. (Selected Papers)

Compiler Correctness Proofs

We have worked on a number of projects in this area. Our work of the early 80's established a flexible method for the correctness of semantics-based compilers. In recent years, we have attempted to make these techniques more applicable in several ways:

Our student Dino Oliva developed methods toward bridging the gap between typical semantics-directed abstract machines, which typically manipulate trees, and the standard structures of activation records, static and dynamic chains, etc. [Oliva's ftp directory] [Our LFP '92 paper]

As part of a cooperative project with the Mitre Corporation, we applied this technique to prove the correctness of a compiler for PreScheme, a dialect of Scheme tailored for systems programming, as part of a verified implementation of Scheme called VLisp. This research was published as a special double issue of the journal Lisp and Symbolic Computation [ftp directory] [Introduction to the report]

With David Gladstein, we extended these results to prove the correctness of a simple compiler for a parallel language. [CONCUR '96 paper]

With Paul Steckler, we developed an interprocedural flow analysis for compilers that are capable of designing a custom calling sequence for each procedure or method. The problem here is that, in higher-order and object-oriented languages, several different procedures may be called from the same site. Our flow analysis ensures that the specialized calling protocol used for each procedure matches the protocol used at each of its possible call sites. [TOPLAS paper]

Complexity of Type Inference Problems

With O'Keefe, Palsberg and Tiuryn, we have considered a number of type inference problems and their complexity.

Last modified: Mon Jan 2 14:20:04 EST 2006
Report problems to Mitch Wand