Proof Theory and Theoretical Computer Science
Special session A25 of the 2nd AMS-UMI International Joint Meeting [Palermo, July 23-24 2024]
The special session A25 on Proof Theory and Theoretical Computer Science is part of the 2nd AMS-UMI International Joint Meeting, which will be hosted by the University of Palermo from July 23 to July 26 2024. The session will be held on July 23 and July 24. The meeting is sponsored by the AMS (American Mathematical Society), the UMI (Unione Matematica Italiana), the Department of Mathematics and Computer Science and the Department of Engineering. The session is sponsored by Lysm.
Check the meeting site for all the relevant information (e.g. the program committee, the local committee, how to reach Palermo, where to find accommodation, the venue, etc.).
Topics of interest
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.
Scope of the session
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.).