Skip to main content
Home

Main navigation

  • Home
  • Series
  • People
  • Depts & Colleges
  • Open Education

Main navigation

  • Home
  • Series
  • People
  • Depts & Colleges
  • Open Education

Foundations of Strong Call by Need

Series
International Conference on Functional Programming 2017
Video Embed
Thibaut Balabonski (LRI, France and University of Paris-Sud, France) gives the third talk in the second panel, Foundations of Higher-Order Programming, on the 2nd day of the ICFP conference.
Co-written by 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 (IRIF/University of Paris Diderot, France).

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.

More in this series

View Series
International Conference on Functional Programming 2017

How to Prove Your Calculus Is Decidable: Practical Applications of Second-Order Algebraic Theories and Computation

Makoto Hamana (Gunma University, Japan), gives the first talk in the second panel, Foundations of Higher-Order Programming, on the 2nd day of the ICFP conference.
Previous
International Conference on Functional Programming 2017

No-Brainer CPS Conversion

Milo Davis (Northeastern University, USA) gives the fourth talk in the second panel, Foundations of Higher-Order Programming, on the 2nd day of the ICFP.
Next
Licence
Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK: England & Wales; http://creativecommons.org/licenses/by-nc-sa/2.0/uk/

Episode Information

Series
International Conference on Functional Programming 2017
People
Thibaut Balabonski
Keywords
computing
programming
Biomedical technology
Department: Department of Computer Science
Date Added: 15/01/2018
Duration: 00:18:59

Subscribe

Apple Podcast Video Video RSS Feed

Download

Download Video

Footer

  • About
  • Accessibility
  • Contribute
  • Copyright
  • Contact
  • Privacy
'Oxford Podcasts' Twitter Account @oxfordpodcasts | MediaPub Publishing Portal for Oxford Podcast Contributors | Upcoming Talks in Oxford | © 2011-2022 The University of Oxford