We present a methodology for deriving a reduction semantics from an equational theory. This methodology is simple and it scales to arbitrarily complex cases. Our starting point is a compositional, big-step specification of a deterministic reduction strategy. We then mechanically derive the key components of a reduction semantics: an optimal grammar of evaluation contexts, a proof of the unique decomposition property, and small-step implementations of the decomposition function and of the recomposition function. The resulting reduction semantics is ``refocus-ready,'' i.e., it is in a form that makes it very simple to derive a corresponding abstract machine, which is traditionally perceived and presented as a major endeavor. The methodology uses two off-the-shelf program transformations: the CPS transformation and defunctionalization. We present three applications: arithmetic expressions, the lambda-calculus with exceptions, and JavaScript, which we extend with coroutines in passing.
Joint work with Ian Zerny.
Olivier Danvy is interested in all aspects of programming languages, including programming. His other mother is the Universite Pierre et Marie Curie (Paris VI: PhD, 1986) and his other mother in law is Aarhus University (DSc, 2006), where he is currently supervising his 22nd PhD student.