Homotopy Type Theory: A Gentle Introduction

Relatore:  Marco Benini - Università degli Studi dell’Insubria
  lunedì 25 settembre 2023 alle ore 16.00 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












































































Titolo Formato  (Lingua, Dimensione, Data pubblicazione)
CV Marco Benini  pdfpdf (it, 163 KB, 12/09/23)

Andrea Masini

Referente esterno
Data pubblicazione
12 settembre 2023

Offerta formativa