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

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.