Write a Blog >>
APLAS 2019
Sun 1 - Wed 4 December 2019 Bali, Indonesia
Mon 2 Dec 2019 16:00 - 16:30 at Bali Room - Semantics Chair(s): Atsushi Igarashi

We present new proofs—formalized in the Coq proof assistant—of the correspondence among call-by-need and (various definitions of) call-by-name evaluations of lambda-calculus with mutually recursive bindings.

For non-strict languages, the equivalence between the high-level specification (call-by-name) and the actual implementation (call-by-need) is of foundational interest. A particular milestone is Launchbury’s natural semantics of call-by-need evaluation and proof of its adequacy with respect to call-by-name denotational semantics, which are recently formalized in Isabelle/HOL by Breitner (2018). Equational theory by Ariola et al. is another well-known formalization of call-by-need. Mutual recursion is especially challenging for their theory: reduction is complicated by the traversal of dependency (the “need” relation), and the correpondnence of call-by-name and call-by-need reductions becomes non-trivial, requiring sophisticated structures such as graphs or infinite trees.

In this paper, we give arguably simpler proofs solely based on (finite) terms and natural semantics, which are easier to handle for proof assistants (Coq in our case). Our proofs can be summarized as follows: (1) we prove the equivalence between Launchbury’s call-by-need semantics and heap-based call-by-name natural semantics, where we define a sufficiently (but not too) general correspondence between the two heaps, and (2) we also show the correspondence among three styles of call-by-name semantics: (i) the natural semantics used in (1); (ii) closure-based natural semantics that informally corresponds to Launchbury’s denotational semantics; and (iii) conventional substitution-based semantics.

Mon 2 Dec

Displayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change

15:30 - 17:00
SemanticsResearch Papers at Bali Room
Chair(s): Atsushi Igarashi Kyoto University, Japan
15:30
30m
Talk
Factorization and Normalization, Essentially
Research Papers
Beniamino Accattoli Inria & Ecole Polytechnique, Claudia Faggian IRIF, Giulio Guerrieri University of Bath
16:00
30m
Talk
Formal Verifications of Call-by-Need and Call-by-Name Evaluations with Mutual Recursion
Research Papers
Masayuki Mizuno Tohoku University , Eijiro Sumii Tohoku University
16:30
30m
Talk
Recursion Schemes in Coq
Research Papers
Kosuke Murata Kyushu Institute of Technology , Kento Emoto Kyushu Institute of Technology