Joint work with Olivier Danvy, Kevin Millikin and Johan Munk.


Starting from the standard call-by-need reduction for the λ-calculus that is common to Ariola, Felleisen, Maraist, Odersky, and Wadler, we inter-derive a series of hygienic semantic artifacts: a reduction-free stateless abstract machine, a continuation-passing evaluation function, and what appears to be the first heapless natural semantics for call-by-need evaluation. Furthermore we observe that a data structure and a judgment in this natural semantics are in defunctionalized form. The refunctionalized counterpart of this evaluation function is an extended direct semantics in the sense of Cartwright and Felleisen.

Overall, the semantic artifacts presented here are simpler than many other such artifacts that have been independently worked out, and which require ingenuity, skill, and independent soundness proofs on a case-by-case basis. They are also simpler to inter-derive because the inter-derivational tools (e.g., refocusing and defunctionalization) already exist.


Olivier Danvy, Kevin Millikin, Johan Munk, and Ian Zerny. On Inter-deriving Small-step and Big-step Semantics: A Case Study for Storeless Call-by-need Evaluation. Theoretical Computer Science, 435:21–42, 2012. [DOI], [BIB], [PDF].
Olivier Danvy, Kevin Millikin, Johan Munk, and Ian Zerny. Defunctionalized Interpreters for Call-by-Need Evaluation. In Matthias Blume, Naoki Kobayashi and Germán Vidal, editors, Functional and Logic Programming, 10th International Symposium, FLOPS 2010. LNCS, 6009, Springer, April 2010, 240–256. [DOI], [BIB], [PDF].

Slides from the talk at FLOPS’10. April 19, 2010, Sendai, Japan.

Official website and weblog for FLOPS’10.