Computer Sciences
Time and Space for the Lambda Calculus
When:
31 July - 11 August 2023
School:
ESS in Logic, Language and Information
Institution:
University of Ljubljana
City:
Country:
Language:
English
Credits:
0 EC
Fee:
490 EUR
About
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
Fee
490 EUR, Early student registration
Fee
690 EUR, Early non-academic registration
Interested?
When:
31 July - 11 August 2023
School:
ESS in Logic, Language and Information
Institution:
University of Ljubljana
Language:
English
Credits:
0 EC