We formally verify an abstract machine for a call-by-value -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.
CITATION STYLE
Kunze, F., Smolka, G., & Forster, Y. (2018). Formal Small-Step Verification of a Call-by-Value Lambda Calculus Machine. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11275 LNCS, pp. 264–283). Springer Verlag. https://doi.org/10.1007/978-3-030-02768-1_15
Mendeley helps you to discover research relevant for your work.