Formal Small-step Verification of a Call-by-value Lambda Calculus Machine

TL;DR

This paper presents a formal verification of an abstract machine for call-by-value lambda calculus, demonstrating correctness through stepwise refinement and Coq proofs, enhancing reliability of lambda calculus implementations.

Contribution

It introduces a formal, verified refinement process for an abstract machine handling lambda calculus, from naive to optimized heap-based structures.

Findings

Correctness of each refinement step verified in Coq

Successful formalization of small-step semantics

Structured sharing in closures improves efficiency

Abstract

We formally verify an abstract machine for a call-by-value lambda-calculus with de Bruijn terms, simple substitution, and small-step semantics. We follow a stepwise refinement approach starting with a naive stack machine with substitution. We then refine to a machine with closures, and finally to a machine with a heap providing structure sharing for closures. We prove the correctness of the three refinement steps with compositional small-step bottom-up simulations. There is an accompanying Coq development verifying all results.