Formal verification of the correspondence between call-by-need and call-by-name

Masayuki Mizuno, Eijiro Sumii

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

Abstract

We formalize the call-by-need evaluation of λ-calculus (with no recursive bindings) and prove its correspondence with call-by-name, using the Coq proof assistant. It has been long argued that there is a gap between the high-level abstraction of non-strict languages—namely, call-by-name evaluation—and their actual call-by-need implementations. Although a number of proofs have been given to bridge this gap, they are not necessarily suitable for stringent, mechanized verification because of the use of a global heap, “graph-based” techniques, or “marked reduction”. Our technical contributions are twofold: (1) we give a simpler proof based on two forms of standardization, adopting de Bruijn indices for representation of (non-recursive) variable bindings along with Ariola and Felleisen’s small-step semantics, and (2) we devise a technique to significantly simplify the formalization by eliminating the notion of evaluation contexts—which have been considered essential for the call-by-need calculus—from the definitions.

Original languageEnglish
Title of host publicationFunctional and Logic Programming - 14th International Symposium, FLOPS 2018, Proceedings
EditorsJohn P. Gallagher, Martin Sulzmann, John P. Gallagher
PublisherSpringer Verlag
Pages1-16
Number of pages16
ISBN (Print)9783319906850
DOIs
Publication statusPublished - 2018 Jan 1
Event14th International Symposium on Functional and Logic Programming, FLOPS 2018 - Nagoya, Japan
Duration: 2018 May 92018 May 11

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10818 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other14th International Symposium on Functional and Logic Programming, FLOPS 2018
CountryJapan
CityNagoya
Period18/5/918/5/11

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Formal verification of the correspondence between call-by-need and call-by-name'. Together they form a unique fingerprint.

  • Cite this

    Mizuno, M., & Sumii, E. (2018). Formal verification of the correspondence between call-by-need and call-by-name. In J. P. Gallagher, M. Sulzmann, & J. P. Gallagher (Eds.), Functional and Logic Programming - 14th International Symposium, FLOPS 2018, Proceedings (pp. 1-16). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10818 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-90686-7_1