Logics and Type Theory: essays dedicated to Stefano Berardi on the occasion of his 1000000th birthday

TL;DR

This collection of essays celebrates Stefano Berardi's contributions to proof theory and type theory, highlighting recent advances and ongoing research in constructive logic, dependent types, and cyclic proofs.

Contribution

It compiles recent research by Stefano Berardi's colleagues, showcasing novel developments and perspectives in proof and type theories.

Findings

Advances in cyclic proofs and their applications

Development of dependent type systems for constructive mathematics

New insights into the foundations of computation

Abstract

Proof Theory and Type Theory are two branches of mathematical logic and theoretical computer science that explore the structure of mathematical proofs and the foundations of computation. Both are crucial for understanding formal systems, programming languages, and constructive mathematics. Stefano Berardi is an influential researcher in these fields, particularly known for his work on constructive logic, dependent types, and more recently, cyclic proofs. These proceedings intend to collect papers by researchers who are active in the field and often have been coauthors of Stefano, aimed to illustrate the achievements and the perspectives of this research area.