Tue 5 Sep 2017 14:07 - 14:30 at L1 - Foundations of Higher-Order Programming Chair(s): Gabriel Scherer
Algorithms that convert direct-style lambda-calculus terms to their equivalent terms in continuation-passing style (CPS) typically introduce so-called “administrative redexes:” useless artifacts of the conversion that must be cleaned up by a subsequent pass over the result to reduce them away. We present a simple, linear-time algorithm for CPS conversion that introduces no administrative redexes. In fact, the output term is a normal form in a reduction system that generalizes the notion of “administrative redexes” to what we call “no-brainer redexes,” that is, redexes whose reduction shrinks the size of the term. We state the theorems which establish the algorithm's desireable properties, along with sketches of the full proofs.
Tue 5 SepDisplayed time zone: Belfast change
Tue 5 Sep
Displayed 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 |