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

2012/02/14 by Wouter Swierstra
Computer Science · #cs.PL

paper · pdf · doi:10.4204/eptcs.76.10

published as EPTCS 76, 2012, pp. 163-177 · In Proceedings MSFP 2012, arXiv:1202.2407

arxiv created 2012/02/14 · arxiv updated 2012/02/15

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.

Citations

• Proceedings Fourth Workshop on Mathematically Structured Functional Programming