BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Eric Finster (University of Birmingham)
DTSTART:20220902T150000Z
DTEND:20220902T161500Z
DTSTAMP:20260423T005705Z
UID:CIRGET/70
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/CIRGET/70/">
 Homotopy Theory and Constructive Mathematics</a>\nby Eric Finster (Univers
 ity of Birmingham) as part of CRM - Séminaire du CIRGET / Géométrie et 
 Topologie\n\n\nAbstract\nConstructive mathematicians and computer scientis
 ts have long been\ninterested in logical theories in which all mathematica
 l statements\nhave computational content.  In such systems\, any proof of 
 the\nexistence of some natural number automatically gives an algorithm for
 \ncomputing the number.  Most modern computer "proof assistants"\, that\ni
 s\, programs aimed at helping the user construct and verify the\ncorrectne
 ss of mathematical statements\, are based on a class of such\nsystems call
  *type theories*.\n\nAround 15 years ago\, however\, it was discovered tha
 t the way type\ntheories represent equality meant that\, rather than descr
 ibing\nconstructive *sets*\, these systems should more properly be thought
  of\nas describing constructive *homotopy types*.  This has led to a numbe
 r\nof new connections between homotopy theory\, higher category theory\,\n
 computer science and logic.  In this talk\, I will describe some of\nthese
  ideas and the results that they have led to.\n
LOCATION:https://researchseminars.org/talk/CIRGET/70/
END:VEVENT
END:VCALENDAR