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.
Swierstra REF formally verifies the correctness of a Krivine machine for simply typed λ-calculus in the dependently typed programming language Agda.
From Mathematics to Abstract Machine: A formal derivation of an executable Krivine machine
EPTCS 76, 2012, pp. 163-177
Computer Science Mathematics