HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information

# A strong call-by-need calculus

2 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
Inria Saclay - Ile de France, LMF - Laboratoire Méthodes Formelles
Abstract : We present a call-by-need λ-calculus that enables strong reduction (that is, reduction inside the body of abstractions) and guarantees that arguments are only evaluated if needed and at most once. This calculus uses explicit substitutions and subsumes the existing strong-call-by-need strategy, but allows for more reduction sequences, and often shorter ones, while preserving the neededness. The calculus is shown to be normalizing in a strong sense: Whenever a λ-term $t$ admits a normal form $n$ in the λ-calculus, then any reduction sequence from $t$ in the calculus eventually reaches the normal form $n$. We also exhibit a restriction of this calculus that has the diamond property and that only performs reduction sequences of minimal length, which makes it systematically better than the existing strategy.
Keywords :
Document type :
Conference papers

https://hal.inria.fr/hal-03149692
Contributor : Thibaut Balabonski Connect in order to contact the contributor
Submitted on : Tuesday, May 4, 2021 - 10:45:11 AM
Last modification on : Friday, February 4, 2022 - 3:08:34 AM

### Files

main.pdf
Files produced by the author(s)

### Citation

Thibaut Balabonski, Antoine Lanco, Guillaume Melquiond. A strong call-by-need calculus. FSCD 2021 - 6th International Conference on Formal Structures for Computation and Deduction, Jul 2021, Buenos Aires, Argentina. pp.1-22, ⟨10.4230/LIPIcs.FSCD.2021.9⟩. ⟨hal-03149692v2⟩

Record views