Homotopy Type Theory (HoTT) is a new approach to foundations of logic, programming and mathematics. It has an increasingly powerful impact on the development of the modern type-theory based tools for programming and verification, such as Coq and Agda proof assistants/certified programming environments. The idea of the seminar is to provide a primer in HoTT and related extensions of Martin-Löf Type Theory (MLTT) such as Cubical Type Theory (more computational in nature than HoTT) and use the corresponding material to practice and improve research skills, such as being able to work with the literature, comprehend scientific texts, summarize and explain the material studied in front of an audience.

We regard the HoTT book (https://homotopytypetheory.org/book) as a unifying background reference, but plan to propose as bases for the actual presentations, tutorials and accessible research articles — see below for a tentative list of sources.

Moreover, we intend to involve proof assistants, based on dependent type theories, to practice and illustrate main ideas and principles. The topics will be discussed and distributed between students depending on their background and interests. We expect a certain degree of flexibility in presentation formats, including at least talks with prepared slides and tool demonstration sessions.

We’re scheduled for Mi, 14:15 – 15:45 in Übung 3 / 01.252-128. First meeting: 19.10.

Previous Edition

Registration

Via StudOn: https://www.studon.fau.de/crs4626834.html

Running Plan of the Talks

TBA

Sources