Workshop on Categorical Logic and Univalent Foundations


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