TY - GEN
T1 - Formal verification of the correspondence between call-by-need and call-by-name
AU - Mizuno, Masayuki
AU - Sumii, Eijiro
N1 - Funding Information:
Acknowledgments. We thank the anonymous reviewers for valuable comments and suggestions. This work was partially supported by JSPS KAKENHI Grant Number 15H02681 and 16K12409.
Publisher Copyright:
© 2018, Springer International Publishing AG, part of Springer Nature.
PY - 2018
Y1 - 2018
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85046731241&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85046731241&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-90686-7_1
DO - 10.1007/978-3-319-90686-7_1
M3 - Conference contribution
AN - SCOPUS:85046731241
SN - 9783319906850
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 1
EP - 16
BT - Functional and Logic Programming - 14th International Symposium, FLOPS 2018, Proceedings
A2 - Gallagher, John P.
A2 - Sulzmann, Martin
A2 - Gallagher, John P.
PB - Springer Verlag
T2 - 14th International Symposium on Functional and Logic Programming, FLOPS 2018
Y2 - 9 May 2018 through 11 May 2018
ER -