Types, Sets and Constructions

Explore advanced topics in constructive mathematics, type theory, and proof theory through this comprehensive summer school lecture series from the Hausdorff Research Institute for Mathematics. Delve into constructive algebra with Thierry Coquand's three-part series covering fundamental principles and applications of algebraic structures in constructive settings. Master the extraction of computational information from mathematical proofs through Ulrich Kohlenbach's detailed examination of proof mining techniques and their practical applications. Gain deep insights into intuitionistic type theory with Peter Dybjer's systematic presentation of the foundations, syntax, and semantics of Martin-Löf type theory. Discover the connections between constructive mathematics and univalent foundations through Martin Hötzel Escardó's exploration of how univalent type theory provides a computational foundation for constructive mathematical practice. Learn from leading experts in the field as they present cutting-edge research and fundamental concepts at the intersection of logic, computer science, and mathematics, with each speaker delivering three comprehensive lectures that build progressively from foundational concepts to advanced applications and current research directions.