Homotopy Type Theory: A Gentle Introduction

Speaker:  Marco Benini - Università degli Studi dell’Insubria
  Monday, September 25, 2023 at 4:00 PM Aula G (presenza e da remoto)

Abstract: Homotopy Type Theory (HoTT) is, syntactically, Martin-Löf Type Theory (MLTT) plus the axiom called “univalence”. Hence, it is, at the same time, an abstract functional programming language, a logical system, and a synthetic way to describe homotopy spaces. The seminar introduces the type system, focusing on the homotopy interpretation, univalence, and higher inductive types, i.e., the main novelties of HoTT with respect to MLTT. The seminar aims at providing the fundamental ideas of HoTT to mathematicians and computer scientists willing to understand what is HoTT without the burden of a formal, in-depth presentation.

Il Dott. Marco Benini è ricercatore di Logica Matematica (MAT01) del Dipartimento di Scienza e Alta Tecnologia
Università degli Studi dell’Insubria

Join Zoom Meeting https://univr.zoom.us/j/93171239033?pwd=cWpaUTJKTTZ1alUvanl3YXFLVHY0Zz09 Meeting ID: 931 7123 9033 Passcode: 212051

Referente: Andrea Masini












































































Title Format  (Language, Size, Publication date)
CV Marco Benini  pdfpdf (it, 163 KB, 12/09/23)

Programme Director
Andrea Masini

Publication date
September 12, 2023