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 contributionpeer-review

1 Citation (Scopus)


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
Number of pages16
ISBN (Print)9783319906850
Publication statusPublished - 2018
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


Conference14th International Symposium on Functional and Logic Programming, FLOPS 2018


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