25-27 January, Universidade de Aveiro, Aveiro, Portugal

Patrick Baillot (CNRS & ENS Lyon, France)

From linear logic to types for implicit computational complexity

Abstract: Linear logic provides a fine-grained logical system to study the dynamics of computation in lambda-calculus. In particular it gives a logical status to the duplication of arguments, thanks to a specific modality. This has triggered logical approaches to implicit computational complexity, a research field aiming at characterizing complexity classes without refering to resource bounds. In this course we will present a guided tour of the contributions of linear logic to implicit computational complexity. We will try to highlight the key ideas of Elementary and Light linear logic through the study of proof-nets and their reduction. We will also show how these logics give rise to type systems for lambda-calculus, ensuring that well-typed programs admit certain time complexity bounds.