  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.
