11 August 2023
Time and Space for the Lambda Calculus
The lambda calculus is the core model behind functional programs and proof assistants, as well as a formalism for representing the proofs of intuitionistic logic. Finding reasonable time and space complexity measures for the lambda calculus, that is, measures that are equivalent to those of Turing machines, have been two long-standing problems, solved only in 2014 (for time) and 2022 (for space). The course aims at explaining three aspects of this topic: 1) The difficulties behind these problems; 2) The tools to solve them, which are based on an abstract theory of implementations of the lambda calculus; 3) How the time and space cost of terms can be captured via type systems for lambda-terms, namely via multi types, a variant of standard type systems for the lambda-calculus.
Course leader
Beniamino Accattoli
Target group
Students
Fee info
EUR 490: Early student registration
EUR 690: Early non-academic registration
Scholarships
There are several scholarship options which you can read about on our website.