Proof and Computation

Here is the collection of the course material for the autumn school Proof and Computation, held during 20-26 September 2019 in Herrsching, Germany.

Courses

• Ingo Blechschmidt: Generalized Spaces for Constructive Algebra (slides are available at Ingo's webpage)
• Stefania Centrone: Proof Theory
• Thierry Coquand: Applications of Type Theory to Univalent Mathematics (see above)
• Anton Freund: Dilators (slides are available at Anton's webpage)
• Tatsuji Kawai: Concepts of Continuity (see above)
• Wolfgang Küchlin: Boolean SAT-Solving, with Applications to Automotive Configuration (see above)
• Dominique Larchey-Wendling: Extraction of Programs in Coq (slides and Coq codes are available at Dominique's GitHub repository)

Working groups

• Ingo Blechschmidt: Tutorial on Agda (codes are available at Ingo's webpage)
• Florian Steinberg: Extracting continuity information in proof assistants
• Dominique Larchey-Wendling: Coq (1) install via Opam (2) cycle detection (3) dfs correctness (see Dominique's GitHub repository)
• Franziskus Wiesnet: Tutorial on Minlog
• Marlou Gijzen and Jinghui Tao: Kolmogorov/Algorithmic complexity (see above)
• Peter Schuster: Learning, resolution, dynamic
• Chuangjie Xu: Computing moduli of continuity in Agda (see above)