Some of My Research Interests

Over the years, I have been in a variety of problems associated with semantics of programming languages. Here is a selected list, in roughly reverse chronological order.

Automatic Differentiation

I am currently investigating the semantics of automatic differentiation, a technology that is a key to both modern "deep learning" and "differentiable programming."

Probabilistic Programming

I worked with a team at BAE Systems and Tufts University to bring the benefits of modern programming-language technology to probablistic programming. This work was funded by DARPA.

Language-Based Program Security

As part of the DARPA CRASH program, I worked with the Gnosys and SAFE teams, trying to develop verifiably-secure software systems. My particular interest in this area is user-facing security: how does one specify user-facing security properties and then verify them, using whatever security mechanisms are available in the language? Unfortunately, this project has terminated, but I am still interested in the topic and am waiting for the right collaborator.

Binding-Safe Programming

The aim of this work is to create tools and techniques for writing meta-programs that are guaranteed to respect the scope of all bound variables. The work is intended for application in a Scheme-like macro system, but it has wider applicability. Papers: ICFP 2014, ESOP 2008

Bisimulations and Contextual Equivalence

This work aimed at using bisimulations to prove the contextual equivalence of untyped, higher-order imperative programs. We developed a new notion of bisimulation that leads to smaller and more tractable relations than previous methods. We were also able to handle examples with higher-order procedures, which pose difficulties for existing methods. Papers: POPL 2006, ESOP 2006, FOOL 2007

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 also wrote a short paper about the Krivine Machine, which has to do with operational semantics, though not (so far) about monads.

Aspect-Oriented Programming

Aspect-oriented programming (AOP) is a technology for allowing adaptation of program units across module boundaries. We developed a semantics for advice and dynamic join points in a subset of AspectJ. We haven't looked at this topic in a while, but it would be nice to have models that are mathematically cleaner than this one, and to develop program analyses for aspect-oriented programming languages. Papers: ICFP 2003 (Invited Talk), TOPLAS 2004

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

Our work of the early 80's (POPL 1982, 1983; TOPLAS 1982; I&C 1983) established a flexible method for the correctness of semantics-based compilers. We spent most of the rest that decade trying to make that development more applicable. 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 . At the time, this was the largest compiler-correctness project ever attempted. (Selected Papers)


In the 70's and 80's, we were one of the early explorers of the concept of continuations. My LFP 1980 paper established the now-standard connection between the mathematical notion of a continuation and the operational notion of a thread. My JACM 1980 paper showed how continuations could be used to assemble program contexts for optimization and transformation. This established for our later work on combinator-based compilers. With Friedman and Haynes, we explored variant notions of continuations and coroutines. Papers: J. Comp. Langs. 1986, LFP 1984, Logic of Programs 1983, JACM 1980, LFP 1980 (reprinted as HOSC 1999).


In our LASC 1988 paper, we gave the first denotational semantics of a fully reflective language, which we called Brown. Our LASC 1998 paper established that even a small amount of reflection was enough to make contextual equivalence trivial.


In our POPL 1987 paper, we gave the first formal definition of macro-by-example, which became the basis for Scheme's syntax-rules macro facility.

Last modified: Mon Nov 25 23:25:30 Eastern Standard Time 2019
Report problems to Mitch Wand