Proof Theory and Theoretical Computer Science

• Linear Logic and its applications;

• Type theory, including Homotopy Type Theory;

• Category Theory in Proof Theory and in Programming Languages;

• Extensions of the Curry-Howard Paradigm, Session Types and Concurrency;

• Proof complexity, Implicit computational complexity, Bounded Arithmetic;

• Automated reasoning: Proof compression, decidability and decision procedures, tableaux systems;

• Proof exchange, concept alignment and proof assistant interoperability;

• Realizability, Semantic types, Constructive Semantics, Classical Realizability.

After the unquestionable role played by Logic in the birth of Computer Science at the beginning of last century, a second period of strong interactions between one among the oldest disciplines of human knowledge and one among the most recent ones occurred in the sixties with the discovery of the so-called Curry-Howard correspondence between proofs (of a particular logical system) and programs (of a paradigmatic programming language).

An example of the fruitfulness of this interaction is type theory: the old idea of Russell to avoid paradoxes of set theory was later used in the framework of Church’s Lambda-Calculus to control its computational power. Later on, Martin Löf proposed intuitionistic type theory as a foundation for constructive mathematics and Thierry Coquand introduced the calculus of constructions, at the base of the interactive theorem prover Coq. The vitality of type theory is also witnessed by the recent inception of Homotopy Type Theory (HoTT) in the landscape.

Another striking example is the birth of Linear Logic (at the end of the eighties) that is at the crossroad of traditional Proof Theory and Theoretical Computer Science: on the one hand it reveals a new structure underlying Logic and computational processes in general thus contributing to Proof Theory and Theoretical Computer Science in the most fundamental sense, and on the other hand it brings new concepts and tools that have been used in various research areas in the last decades (theory of programming languages, implicit computational complexity, concurrency, game semantics, category theory, philosophy, linguistics, etc.).