### 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