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

TL;DR

This paper formally derives an executable Krivine machine from a small step interpreter for simply typed lambda calculus using Agda, bridging theoretical semantics and practical implementation.

Contribution

It introduces a formal derivation process of the Krivine machine from a lambda calculus interpreter within a dependently typed language.

Findings

Successfully derived an executable Krivine machine from a small step interpreter.

Demonstrated the correctness of the derivation within Agda.

Bridged the gap between theoretical semantics and executable models.

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.