# Formal Verification of a Call-by-value Lambda Calculus Machine

## Fabian Kunze, Gert Smolka, Yannick Forster

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.