Formal small-step verification of a call-by-value lambda calculus machine

DOI10.1007/978-3-030-02768-1_15MaRDI QIDQ6166150zbMATH OpenFDO

Authors Fabian Kunze, Gert Smolka, Yannick Forster

Publication date 2 August 2023

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1806.03205

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60)

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.

Recommendations

• Formal verification of the correspondence between call-by-need and call-by-name
• An abstract machine for strong call by value
• Call-by-value lambda calculus as a model of computation in Coq
• From operational semantics to abstract machines
• The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: a proof via corresponding calculus

Cited in

(6)

• Weak call-by-value lambda calculus as a model of computation in Coq
• Call-by-value lambda calculus as a model of computation in Coq
• Step indexed realizability semantics for a call-by-value language based on basic combinatorial objects
• scientific article; zbMATH DE number 800564 (Why is no real title available?)
• A verified cost model for call-by-push-value
• On the equivalence between small-step and big-step abstract machines: a simple application of lightweight fusion

This page was built for publication: Formal small-step verification of a call-by-value lambda calculus machine

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6166150)