Colloquium
The event has passed

Colloquium, Mathematical Sciences

Thierry Coquand, University of Gothenburg/Chalmers: Dependent Types, Homotopy and Formalisation of Mathematics

Add to OutlookAdd to Google Calendar

Overview

The event has passed
  • Date:Starts 13 November 2023, 15:30Ends 13 November 2023, 16:30
  • Location:
    Euler, Physics building, Skeppsgränd 3
  • Language:English

Abstract
Dependent Type Theory is a formalism introduced by the mathematician N.G. de Bruijn in order to represent and check mathematical reasoning on a computer. (This formalism is now used in the system Lean, popularised by Kevin Buzzard.) Around 20 years ago, V. Voevodsky discovered unexpected connections between this formalism and homotopy theory. I will first try to explain these connections, and then survey some recent developments around these ideas.

Note: Colloquium fika is served in the lunchroom from 15:00

Michael Björklund
  • Professor, Analysis and Probability Theory, Mathematical Sciences
Contact