Hauptinhalt

Topinformationen

Personen

Reading Club: Homotopy Type Theory

8.30504

Dozenten

Beschreibung

Proof assistants support mathematicians and programmers in developing formal proofs in an interactive human-machine collaboration. Recent efforts in Artificial Intelligence target at further automatizing this process by applying general problem solving strategies or machine learning. Several proof assistants, like Coq, Agda, and Idris, are based on type theory as a formal framework. Homotopy Type Theory (HoTT) is a relatively new branch of mathematics that aims at providing a solid foundation for such approaches.

In this reading club we will study the original HoTT publication [1] and discuss both, its role as a mathematical foundational framework as well as the ramifications for automated proof checking. This course does not require any specific prior knowledge, but assumes some joy in dealing with formal systems as well as a decent interest in mathematics. People with some background in type theory (e.g. the Martin-Löf version) may gain a premium membership in our club.

To succeed in this course, active participation in our weekly club meetings, including chairing sessions, is required. Meetings should be prepared by contributing to online discussions in the StudIP forum.

[1] https://homotopytypetheory.org/book/

Weitere Angaben

Ort: 50/E07
Zeiten: Di. 16:00 - 18:00 (wöchentlich) - Room 50/E07 would be great!
Erster Termin: Dienstag, 15.04.2025 16:00 - 18:00, Ort: 50/E07
Veranstaltungsart: Seminar (Offizielle Lehrveranstaltungen)