Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
Wed 21 Aug 2019 16:50 - 17:13 at Aurora Borealis - Lambda-Calculus & Teaching Chair(s): Jonathan Protzenko

Call-by-need evaluation, also known as lazy evaluation, provides two key benefits: compositional programming and infinite data. The standard semantics for laziness is Launchbury’s natural semantics [1993], which uses a heap to memoise the results of delayed evaluations. However, the stateful nature of this heap greatly complicates reasoning about the operational behaviour of lazy programs. In this article, we propose an alternative semantics for laziness, clairvoyant evaluation, that replaces the state effect with nondeterminism, and prove this semantics equivalent in a strong sense to the standard semantics. We show how this new semantics greatly simplifies operational reasoning, admitting much simpler proofs of a number of results from the literature, and how it leads to the first denotational cost semantics for lazy evaluation.

Wed 21 Aug

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:50 - 18:00
Lambda-Calculus & TeachingResearch Papers at Aurora Borealis
Chair(s): Jonathan Protzenko Microsoft Research, Redmond
16:50
23m
Talk
Call-By-Need is Clairvoyant Call-By-Value
Research Papers
Jennifer Hackett University of Nottingham, UK, Graham Hutton University of Nottingham, UK
17:13
23m
Talk
Teaching the Art of Functional Programming Using Automated Grading (Experience Report)
Research Papers
Aliya Hameer McGill University, Brigitte Pientka McGill University
17:36
23m
Talk
Lambda: the Ultimate Sublanguage (Experience Report)
Research Papers
Jeremy Yallop University of Cambridge, UK, Leo White Jane Street
DOI Pre-print