School on Formal Mathematics

This one-week school teaches practical theorem proving in the three proof assistants with the greatest coverage of (research) Mathematics: Coq, Isabelle and Lean as well as smaller, more specialized systems. Key people from the research groups have indicated their willingness to teach (and supervise practical formalization attempts) in this school, drawing on tutorial material of the various systems. Participants of the school will be asked to work on small formalization projects which eventually could lead to contributions to formalization libraries. There will be a couple of introductory and special lectures.

Guillaume Allais (University of Strathclyde): Agda

Guillaume Allais: A Quick Tour of Agda

Guillaume Allais: Syntaxes for Binding and their Semantics

Steve Awodey (Carnegie Mellon University): What is HoTT?

Steve Awodey: What is HoTT?

Andrej Bauer (University of Ljubljana): Constructive Mathematics - How to not believe in the Law of Excluded Middle

Andrej Bauer: Constructive Mathematics - How to not believe in the Law of Excluded Middle

Mario Carneiro (Carnegie Mellon University): System Introductions I - Lean

Mario Carneiro: System Introductions I - Lean

Mario Carneiro (Carnegie Mellon University): Lessons for Metamath

Mario Carneiro: Lessons for Metamath

Manuel Eberl (Universität Innsbruck): System Introductions II - Isabelle

Manuel Eberl: System Introductions II - Isabelle

Yannick Forster (Centre Inria de Paris): System Introductions I - Coq

Yannick Forster: System Introductions I - Coq

Peter Koepke (University of Bonn): Naproche

Peter Koepke: System Introductions II - Naproche

Peter Koepke First-Order Mathematics and Naproche

Michael Kohlhase (FAU Erlangen-Nürnberg): System Introductions II - sTeX/ALeA

Michael Kohlhase: System Introductions II - sTeX/ALeA

Michael Kohlhase (FAU Erlangen-Nürnberg): ALeA - Flexiformal Education

Michael Kohlhase: ALeA - Flexiformal Education

Sam Owre (SRI International): PVS

Sam Owre: System Introductions I - PVS

Sam Owre: Modularity in PVS

Josef Urban (CIIRC - CTU): Theorem Proving and AI

Josef Urban: Theorem Proving and AI

Freek Wiedijk (Radboud University): HOL Light

Freek Wiedijk: System Introductions I - HOL

Freek Wiedijk: More on HOL Light

Freek Wiedijk: Even more on HOL Light

Mario Carneiro (Carnegie Mellon University) and Andrej Bauer (University of Ljubljana): Universes in Set/Type Theory

Mario Carneiro and Andrej Bauer: Universes in Set/Type Theory

Back up