Skip to main content

From typed programming languages to synthetic homotopy theory

Posted in
Speaker: 
Félix Loubaton
Affiliation: 
MPIM
Date: 
Thu, 13/06/2024 - 15:00 - 16:00
Location: 
MPIM Lecture Hall
Parent event: 
MPI-Oberseminar

In this talk I'll try to give an overview of (homotopic) type theory, a theory which produces a very important link between computer science and homotopy theory and which is at the heart of modern proof assistants.

We'll start with concrete examples from computer science, which will allow us to introduce Martin-Löf's dependent type theory. We'll then talk about Voevodsky's univalence axiom and finally the interepration of this theory in simplicial sets by Voevodsky, Lumsdaine and Warren.


 

© MPI f. Mathematik, Bonn Impressum & Datenschutz
-A A +A