Ljubljana, Slovenia

Time and Space for the Lambda Calculus

when 31 July 2023 - 11 August 2023
language English
duration 2 weeks
fee EUR 490

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


Fee info

EUR 490: Early student registration
EUR 690: Early non-academic registration


There are several scholarship options which you can read about on our website.