Wouter Swierstra

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.

Sign up or login to leave a comment