Defunctionalized Interpreters for Higher-Order Programming Languages

How does one specify a computation? Some use calculi, the best-known of which is probably the lambda-calculus. Some use abstract machines, i.e. state-transition systems. Some use evaluation functions, i.e. interpreters. Some use compilers towards some byte code and virtual machines operating over this byte code.

How does one check that the various semantic artifacts mentioned just above are compatible with each other? For example, how does one check that a code processor correctly implements a calculus? More generally, how does one design such semantic artefacts?

It is our thesis (*) that in many interesting cases, these semantic artefacts can be derived from each other, and furthermore that the derivations are based on simple program transformations. A technique called 'refocusing' makes it possible to go from one-step reduction to a pre-abstract machine, and from there to a staged abstract machine and then an eval/apply abstract machine, and under some conditions to a push/enter machine. Conversely, a combination of simple program transformations (lambda-lifting, closure conversion, CPS transformation, defunctionalization) makes it possible to mechanically transform interpreters (implementations of denotational semantics and of big-step operational semantics) into abstract machines (implementations of small-step operational semantics). The derivational approach makes it possible to relate one-step reduction and evaluation, and to reconstruct known abstract machines as well as to construct new ones. We will also briefly touch upon compilers and virtual machines.

(*) A real thesis: http://www.brics.dk/~danvy/DSc.html