From Mathematics to Abstract Machine: A formal derivation of an executable Krivine machine

Wouter Swierstra
(Radboud University Nijmegen)

This paper presents the derivation of an executable Krivine abstract machine from a small step interpreter for the simply typed lambda calculus in the dependently typed programming language Agda.

In James Chapman and Paul Blain Levy: Proceedings Fourth Workshop on Mathematically Structured Functional Programming (MSFP 2012), Tallinn, Estonia, 25 March 2012, Electronic Proceedings in Theoretical Computer Science 76, pp. 163–177.
Published: 11th February 2012.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: