Startseite

Program of Workshop on Homotopy Type Theory

For the abstracts click on the titles or see the list of abstracts.

Mit, 10 Feb 2016

10:00 - 11:00
MPIM Lecture Hall
Vladimir Voevodsky
Dependent Type Theories
14:30 - 16:00
MPIM Lecture Hall
Chris Kapulkin
Internal languages of higher categories
16:30 - 18:00
MPIM Lecture Hall
Eric Finster
Higher categories with families

Don, 11 Feb 2016

10:00 - 11:00
MPIM Lecture Hall
Vladimir Voevodsky
Dependent Type Theories
13:30 - 15:00
MPIM Lecture Hall
Benno van den Berg
Fibration categories, the propositional J rule and setoids
15:00 - 16:00
MPIM Lecture Hall
Clemens Berger
Eine Wanderung durch Rainer Vogt's mathematisches Schaffen (A journey through Rainer Vogt's mathematical work) - MPI-Oberseminar jointly with the Workshop on Homotopy Type Theory -
16:30 - 18:00
MPIM Lecture Hall
Peter Lumsdaine
Homotopy theory of type theories

Fre, 12 Feb 2016

10:00 - 11:00
MPIM Lecture Hall
Vladimir Voevodsky
Dependent Type Theories
13:30 - 15:00
MPIM Lecture Hall
Bas Spitters
Cubical sets as a classifying topos
15:30 - 17:00
MPIM Lecture Hall
Ulrik Buchholtz
The quaternionic Hopf fibration in HoTT via a modified Cayley-Dickson construction

Sam, 13 Feb 2016

10:00 - 11:00
MPIM Lecture Hall
Vladimir Voevodsky
Dependent Type Theories
14:30 - 16:00
MPIM Lecture Hall
Egbert Rijke
Aspects of the graph model of homotopy type theory
16:30 - 18:00
MPIM Lecture Hall
Thomas Streicher
Splitting dictoses

Son, 14 Feb 2016

10:00 - 11:00
MPIM Lecture Hall
Vladimir Voevodsky
Dependent Type Theories
13:30 - 14:15
MPIM Lecture Hall
Dan Grayson
The UniMath project
14:15 - 15:00
MPIM Lecture Hall
Simon Huber
The cubical type checker
15:30 - 16:15
MPIM Lecture Hall
Bas Spitters
The Homotopy Type Theory library in Coq
16:15 - 17:00
MPIM Lecture Hall
Andrej Bauer
The Andromeda proof assistant
17:00 - 17:45
MPIM Lecture Hall
Peter Lumsdaine
Formalizing Categories with Attributes in Coq

 

... back to parent event

LaTeX version

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