Course "ADVANCES IN Mathematical Logic. Homotopy Type Theory"

September 28, 2023

Lecturer and Examiner: Dr. Iosif Petrakis

Period: Nov-Dec 2023, Start: Tuesday 07.11.2023

Type of course: Hybrid

Zoom-links: Please send an e-mail to Dr. Iosif Petrakis or to Dr. Giulio Fellin

Venue: Department of Computer Science, University of Verona

Rooms: Auletta Atrio - Borgo Roma - Ca’ Vignal 1 - Strada Le Grazie 15, Verona.

For the lecture of Friday 01.12.2023 only: Aula G - Borgo Roma - Ca’ Vignal 2 - Strada Le Grazie 15, Verona.

Time: Tuesday 14:00-17:00 and Friday 10:00-13:00

Contact: Iosif Petrakis

Number of academic hours: 35

Assessment method: Written exam

Intended audience: Computer scientists and mathematicians (PhD-level and advanced Master’s-level)

Abstract: Martin-Löf’s type theory (MLTT) is a predicative modification of lambda-calculus with many applications to the theory of programming languages. The recent extension of MLTT with the axiom of univalence (UA) by the late Fields medalist Voevodsky reveals surprising connections between homotopy theory and logic. Homotopy Type Theory (HoTT) can be described as MLTT + UA + Higher Inductive Types. HoTT and Category Theory (CaT), are currently among the most actively studied mathematical frameworks for the logical foundations of mathematics and theoretical computer science. The following topics are planned to be covered: introduction to MLTT, function-extensionality axiom, the groupoid model of Hofmann and Streicher, Voevodsky’s axiom of univalence, homotopy n-types, higher inductive types, the fundamental group of the higher circle, relations between HoTT and constructive mathematics, relations between HoTT and CaT.

No prior knowledge of homotopy theory and type theory is required.

Lecture notes will be available.

References:

  1. E. Rijke: Introduction to Homotopy Type Theory, https://arxiv.org/abs/2212.11082, 2022, pre-publication version, which will be published by Cambridge University Press.

  2. I. Petrakis: Logic in Computer Science, Lecture notes, 2022. https://www.mathematik.uni-muenchen.de/~petrakis/LCS.pdf

  3. The Univalent Foundations Program Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Study, Princeton, 2013. https://homotopytypetheory.org/book/