BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Theoretical computer science seminar
SUMMARY:On Cubes and Types - Thorsten Altenkirch (Universi
ty of Nottingham)
DTSTART:20150130T160000Z
DTEND:20150130T170000Z
UID:TALK1662AT
URL:/talk/index/1662
DESCRIPTION:(joint work with Ambrus Kaposi)\n\nHomotopy Type T
heory (HoTT) extends Martin-Loef Type Theory with
the univalence principle\, a strong extensionality
principle that internalizes the idea that equival
ent structures should be considered equal. At the
same time we are lead to view types as higher dime
nsional objects in the sense of homotopy theory.\n
\nDue to its extensional nature HoTT seems ideally
suited to support mathematical abstraction and ma
y hence be indispensable when building large libra
ries of formalized mathematics and verified progra
ms.\n\nCurrently\, HoTT faces one major obstacle:
we do not know how to extend the computational pri
nciples from conventional Type Theory to HoTT. To
address this issue we propose a different way to i
ntroduce equality types in Type Theory as an heter
ogenous equality defined as a logical relation. Th
is approach is clearly related to Bernardy's and M
oulin's internal parametricity and Coquand's and H
uber's cubical set model. Due to the presence of h
igher dimensional cubes in all these approaches we
call this Cubical Type Theory. In the talk I will
give a gentle introduction to cubical type theory
and try to explain how far we got and what remain
s to be done.
LOCATION:CS 245
CONTACT:Neel Krishnaswami
END:VEVENT
END:VCALENDAR