From Mathematics to Abstract Machine: A formal derivation of an executable Krivine machine
arXiv:1202.2924 · doi:10.4204/EPTCS.76.10
Abstract
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 Proceedings MSFP 2012, arXiv:1202.2407