### 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 language | English |
---|---|

Title of host publication | Functional and Logic Programming - 14th International Symposium, FLOPS 2018, Proceedings |

Editors | John P. Gallagher, Martin Sulzmann, John P. Gallagher |

Publisher | Springer Verlag |

Pages | 1-16 |

Number of pages | 16 |

ISBN (Print) | 9783319906850 |

DOIs | |

Publication status | Published - 2018 Jan 1 |

Event | 14th International Symposium on Functional and Logic Programming, FLOPS 2018 - Nagoya, Japan Duration: 2018 May 9 → 2018 May 11 |

### Publication series

Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|

Volume | 10818 LNCS |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Other

Other | 14th International Symposium on Functional and Logic Programming, FLOPS 2018 |
---|---|

Country | Japan |

City | Nagoya |

Period | 18/5/9 → 18/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

*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