Call-by-need calculi are complex to design and reason with. When adding control effects, the very notion of canonicity is irremediably lost, the resulting calculi being necessarily ad hoc. This calls for a design of call-by-need guided by logical rather than operational considerations. Ariola et al. proposed such an extension of call-by-need with control making use of Curien and Herbelin's duality of computation framework.#R##N##R##N#In this paper, Classical by-need is developed as an alternative extension of call-by-need with control, better-suited for a programming-oriented reader.This method is proof-theoretically oriented by relying on linear head reduction LHR --- an evaluation strategy coming from linear logic --- and on the $$\lambda \mu $$λμ-calculus --- a classical extension of the $${\lambda }$$λ-calculus.#R##N##R##N#More precisely, the paper contains three main contributions:LHR is first reformulated by introducing closure contexts and extended to the $${\lambda }{\mu }$$λμ-calculus;it is then shown how to derive a call-by-need calculus from LHR. The result is compared with standard call-by-need calculi, namely those of Ariola---Felleisen and Chang---Felleisen;it is finally shown how to lift the previous item to classical logic, that is from the $${\lambda }$$λ-calculus to the $${\lambda }{\mu }$$λμ-calculus, providing a classical by-need calculus, that is a lazy $${\lambda }{\mu }$$λμ-calculus. The result is compared with the call-by-need with control of Ariola et al.
['Pierre-Marie Pédrot', 'Alexis Saurin']
Classical By-Need