Some of My Research Interests

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)

Continuations

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).

Reflection

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.

Macros

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