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: https://dx.doi.org/10.4204/EPTCS.76.10 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org