Publication details

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

Formal Small-step Verification of a Call-by-value Lambda Calculus Machine

Fabian Kunze, Gert Smolka, Yannick Forster

16th Asian Symposium on Programming Languages and Systems, APLAS 2018, Wellington, New Zealand, December 2-6, pp. 264-283, Springer, December 2018

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.

Link to Coq Formalisation - Preliminary version at arXiv

Download PDF        Show BibTeX               

@INPROCEEDINGS{KunzeEtAl:2018:cbvlcm2,
  title = {Formal Small-step Verification of a Call-by-value Lambda Calculus Machine},
  author = {Fabian Kunze and Gert Smolka and Yannick Forster},
  year = {2018},
  month = {Dec},
  editor = {S. Ryu},
  publisher = {Springer},
  booktitle = {16th Asian Symposium on Programming Languages and Systems, APLAS 2018, Wellington, New Zealand, December 2-6},
  series = {LLNCS 11275},
  pages = {264-283},
  note = {Preliminary version appeared as arXiv:1806.03205},
}

Login to edit