ICFP 2017
Sun 3 - Sat 9 September 2017 Oxford, United Kingdom
Tue 5 Sep 2017 13:45 - 14:07 at L1 - Foundations of Higher-Order Programming Chair(s): Gabriel Scherer

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 Sep Times are displayed in time zone: Belfast change

 13:00 - 14:30 Foundations of Higher-Order ProgrammingResearch Papers at L1 Chair(s): Gabriel SchererNortheastern University 13:0022mTalk How to Prove Your Calculus Is Decidable: Practical Applications of Second-Order Algebraic Theories and ComputationResearch PapersMakoto HamanaGunma University, Japan DOI 13:2222mTalk A Relational Logic for Higher-Order ProgramsResearch PapersAlejandro AguirreIMDEA Software Institute, Spain, Gilles BartheIMDEA Software Institute, Spain, Marco GaboardiUniversity at Buffalo, SUNY, USA, Deepak GargMPI-SWS, Germany, Pierre-Yves StrubÉcole Polytechnique, n.n. DOI 13:4522mTalk Foundations of Strong Call by NeedResearch PapersThibaut BalabonskiLRI, France / University of Paris-Sud, France, Pablo BarenbaumUniversity of Buenos Aires, Argentina / IRIF, France / University of Paris Diderot, France, Eduardo BonelliCONICET, Argentina / Universidad Nacional de Quilmes, Argentina, Delia KesnerIRIF, France / University of Paris Diderot, France DOI 14:0722mTalk No-Brainer CPS ConversionResearch PapersMilo DavisNortheastern University, USA, William MeehanNortheastern University, USA, Olin ShiversNortheastern University, USA DOI