Formal Small-step Verification of a Call-by-value Lambda Calculus Machine
Logic in Computer Science
2019-01-03 v3 Programming Languages
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.
Keywords
Cite
@article{arxiv.1806.03205,
title = {Formal Small-step Verification of a Call-by-value Lambda Calculus Machine},
author = {Fabian Kunze and Gert Smolka and Yannick Forster},
journal= {arXiv preprint arXiv:1806.03205},
year = {2019}
}