We present a call-by-need strategy for computing strong normal forms of open terms (reduction is admitted inside the body of abstractions and substitutions, and the terms may contain free variables), which guarantees that arguments are only evaluated when needed and at most once. The strategy is shown to be complete with respect to $\beta$-reduction to strong normal form. The proof of completeness relies on two key tools: (1) the definition of a strong call-by-need calculus where reduction may be performed inside any context, and (2) the use of non-idempotent intersection types. More precisely, terms admitting a $\beta$-normal form in pure lambda calculus are typable, typability implies (weak) normalisation in the strong call-by-need calculus, and weak normalisation in the strong call-by-need calculus implies normalisation in the strong call-by-need strategy. Our (strong) call-by-need strategy is also shown to be conservative over the standard (weak) call-by-need.
Tue 5 SepDisplayed time zone: Belfast change
13:00 - 14:30 | Foundations of Higher-Order ProgrammingResearch Papers at L1 Chair(s): Gabriel Scherer Northeastern University | ||
13:00 22mTalk | How to Prove Your Calculus Is Decidable: Practical Applications of Second-Order Algebraic Theories and Computation Research Papers Makoto Hamana Gunma University, Japan DOI | ||
13:22 22mTalk | A Relational Logic for Higher-Order Programs Research Papers Alejandro Aguirre IMDEA Software Institute, Spain, Gilles Barthe IMDEA Software Institute, Spain, Marco Gaboardi University at Buffalo, SUNY, USA, Deepak Garg MPI-SWS, Germany, Pierre-Yves Strub École Polytechnique, n.n. DOI | ||
13:45 22mTalk | Foundations of Strong Call by Need Research Papers Thibaut Balabonski LRI, France / University of Paris-Sud, France, Pablo Barenbaum University of Buenos Aires, Argentina / IRIF, France / University of Paris Diderot, France, Eduardo Bonelli CONICET, Argentina / Universidad Nacional de Quilmes, Argentina, Delia Kesner Université de Paris, CNRS, IRIF, France DOI | ||
14:07 22mTalk | No-Brainer CPS Conversion Research Papers Milo Davis Northeastern University, USA, William Meehan Northeastern University, USA, Olin Shivers Northeastern University, USA DOI |