Workshop on Categorical Logic and Univalent Foundations
HOTT16
Useful links
The university:
Logic associations:
Tourism:
Travel:
Registration is close to the main entrace of the School of Mathematics on Level 9, through the door to your left (Reading Room 9.31). Talks will be held in the School of Mathematics, Level 8 Seminar Room, MALL 1&2 (a single room). Coffee will be served in Reading Room 9.31 next to the Common Area on Level 9.
Lunch can be had at the Refectory. There will be an informal dinner on Thursday evening at Akbar's.
For detailed location information, see here.
Wednesday, July 27 | |||||
9:30 | – | 10:00 | Registration | ||
10:00 | – | 11:00 | Plenary: Steve Awodey, a cubical fibrant replacement monad | ||
11:00 | – | 11:30 | Coffee break | ||
11:30 | – | 12:10 | Benno van der Berg, a homotopy-theoretic model of function extensionality in the effective topos | ||
12:10 | – | 12:50 | Paolo Capriotti, presheaf models of two-level type theory | ||
12:50 | – | 14:20 | Lunch break | ||
14:20 | – | 15:20 | Plenary: Robert Harper, computational higher type theory | ||
15:20 | – | 15:50 | Coffee break | ||
15:50 | – | 16:30 | Egbert Rijke, principal equivalence relations | ||
16:30 | – | 17:10 | Nicolai Kraus, higher categorical structures and homotopy coherent diagrams |
Thursday, July 28 | |||||
10:00 | – | 11:00 | Plenary: Matthieu Sozeau, forcing translations in type theory | ||
11:00 | – | 11:30 | Coffee break | ||
11:30 | – | 12:10 | Thierry Coquand, a constructive model of homotopy types | ||
12:10 | – | 12:50 | Christian Sattler, a modular glueing construction | ||
12:50 | – | 14:20 | Lunch break | ||
14:20 | – | 15:20 | Plenary: Andrej Bauer, the Andromeda proof assistant | ||
15:20 | – | 15:50 | Coffee break | ||
15:50 | – | 16:30 | Dimitri Tsementzis, homotopy model theory | ||
19:30 | – | 21:30 | Dinner at Akbar's |
Friday, July 29 | |||||
10:00 | – | 10:40 | Erik Palmgren, categories with families, FOLDS and logic enriched type theory | ||
10:40 | – | 11:10 | Coffee Break | ||
11:10 | – | 11:50 | Andrew Swan, some constructions of split comprehension categories with application to realizability | ||
11:50 | – | 12:30 | Thorsten Altenkirch, homotopy type theory as a foundations for mathematics? | ||
12:30 | – | 14:00 | Lunch break |
© Copyright Leeds 2012