Proof and Computation

Here is the collection of the course material of the autumn school Proof and Computation, held during 26 September to 1 October 2022 in Fischbachau, Germany.

Courses

• Steve Awodey: Categorical Logic
• Marc Bezem: Coherent Logic
• Hajime Ishihara: Reverse Mathematics in Constructive Set Theory
• Stefan Neuwirth: The Philosophy of Dynamic Algebra
• Fredrik Nordvall Forsberg: Universes of Data Types in Constructive Type Theory
• Ingo Blechschmidt: Extraction of Programs from Proofs
• Chuangjie Xu: Various Approaches to Computing Moduli of Continuity

Working Groups

• Franziskus Wiesnet: Implementing a poker engine
• Matthias Hutzler & Ingo Blechschmidt: Introduction to Agda for absolute beginners
• Fredrik Nordvall Forsberg: Internal Language in Agda (reflectionT.agda)
• Josh Chen: Trying to understand / Introduction to synthetic tait computability
• Marc Bezem: Automating coherent logic
• Max Zeuner: Different approaches to schemes (and ongoing formalization projects)
• Fredrik Nordvall Forsberg: Ordinals and continuity