Professor: Beniamino Accattoli
The λ-calculus is the model behind functional programming languages and proof assistants, as well as a proof formalism for intuitionistic logic. Its dynamics is based on a single rewriting rule, β-reduction. The understanding of cost models for the λ-calculus was very limited [BG95, AM98, SGM02, DLM08], untill very recently. The abstract character of the λ-calculus comes at a price, known as size-explosion: there are malicious programs that in a linear number of β-steps produce an exponential output, thus apparently forbidding to take the number of β-steps as a reasonable cost model. Recently, the situation changed. Notably, Accattoli and Dal Lago showed that the number of (leftmost) β-steps is, surprisingly, a reasonable cost model [AL14]. Such a result is the apex of an emerging quantitative theory of β-reduction [ABKL14, ABM14, AC15, AG16, AGK18]. This course will introduce the study of cost models and size-explosion, as well as the basic concepts of the quantitative theory.
Remark: Due to public demand, the course will also include a general introduction to the topic.
1. Introduction to reasonable cost models. Size explosion. Literature on the topic (based on [A18]).
2. Abstract machines and a proof that the call-by-name weak λ-calculus is reasonable ([A16]).
3. The call-by-value case. The open case and its different presentations ([AG16]).
4. The standardisation theorem and the subterm property ([ABKL14],[AL14]).
5. Multi types and evaluation lengths ([AGK18]). Required Background Basics of functional programming, rewriting theory, and logic.
[A16] Beniamino Accattoli. The Complexity of Abstract Machines. WPTE@FSCD 2016, pages 1-15, 2016.
[A18] Beniamino Accattoli. (In)Efficiency and Reasonable Cost Models. Electr. Notes Theor. Comput. Sci. 338, pages 23-43 2018.
[ABM14] Beniamino Accattoli, Pablo Barenbaum, and Damiano Mazza. Distilling abstract machines. In ICFP 2014, pages 363–376, 2014.
[ABKL14] Beniamino Accattoli, Eduardo Bonelli, Delia Kesner, and Carlos Lombardi. A nonstandard standardization theorem. In POPL, pages 659–670, 2014.
[AGK18] Beniamino Accattoli, Stéphane Graham-Lengrand, Delia Kesner. Tight typings and split bounds. In PACMPL 2(ICFP), pages 1-30, 2018.
[AC15] Beniamino Accattoli and Claudio Sacerdoti Coen. On the relative usefulness of fireballs. In LICS 2015, pages 141–155, 2015.
[AG16] Beniamino Accattoli and Giulio Guerrieri. Open call-by-value. In APLAS 2016, pages 206–226, 2016.
[AL14] Beniamino Accattoli and Ugo Dal Lago. Beta reduction is invariant, indeed. In CSL-LICS ’14, pages 8:1–8:10, 2014.
[AM98] Andrea Asperti and Harry G. Mairson. Parallel beta reduction is not elementary recursive. In POPL, pages 303–315, 1998.
[BG95] Guy E. Blelloch and John Greiner. Parallelism in sequential functional languages. In FPCA, pages 226– 237, 1995.
[DLM08] Ugo Dal Lago and Simone Martini. The weak lambda calculus as a reasonable machine. Theor. Comput. Sci., 398(1-3):32–50, 2008. [SGM02] David Sands, J¨orgen Gustavsson, and Andrew Moran. Lambda calculi and linear speedups. In The Essence of Computation, pages 60–84, 2002.
[SGM02] David Sands, Jorgen Gustavsson, and Andrew Moran. Lambda calculi and linear speedups. In The Essence of Computation, pages 60–84, 2002.
All course material can be found at: