A strong call-by-need calculus

We present a call-by-need $\lambda$-calculus that enables strong reduction(that is, reduction inside the body of abstractions) and guarantees thatarguments are only evaluated if needed and at most once. This calculus usesexplicit substitutions and subsumes the existing strong-call-by-need strategy,but allows for more reduction sequences, and often shorter ones, whilepreserving the neededness. The calculus is shown to be normalizing in a strongsense: Whenever a $\lambda$-term t admits a normal form n in the$\lambda$-calculus, then any reduction sequence from t in the calculuseventually reaches a representative of the normal form n. We also exhibit arestriction of this calculus that has the diamond property and that onlyperforms reduction sequences of minimal length, which makes it systematicallybetter than the existing strategy. We have used the Abella proof assistant toformalize part of this calculus, and discuss how this experiment affected itsdesign. In particular, it led us to derive a new description of call-by-needreduction based on inductive rules