Tuesday 11 June (TYPES)

See TYPES 19-program

Wednesday 12 June (joint with TYPES 19):

08:00 Registration and coffee
08:55 Workshop opening by Bjørn Ian Dundas
Session: Invited Talks HoTT-UF and TYPES
09:00 Christian Sattler: Homotopy canonicity
10:00 Break
10:30 Conor McBride: Check the Box!
11:30 Simon Huber: Homotopy Canonicity for Cubical Type Theory
12:30 Lunch
Session: TYPES Contributed Talks on HoTT
14:00 Fabian Ruch and Thierry Coquand: Sheaf Models of Univalent Type Theory
14:15 Martin Escardo: Compact, totally separated and well-ordered types in univalent mathematics
14:30 Anders Mörtberg, Andrea Vezzosi and Andreas Abel: Cubical Agda: A Dependently Typed PL with Univalence and HITs
14:45 Edward Morehouse, G. A. Kavvos and Daniel Licata: A Double-Categorical Perspective on Type Universes
15:00 Ulrik Buchholtz and Jonathan Weinberger: Type-theoretic modalities for synthetic (∞,1)-categories
15:15 Pierre Cagne: Quillen bifibrations and the Reedy construction
15:30 Break
16:00 Evan Cavallo: Cubical Indexed Inductive Types
17:00 Departure from Ingeniørenes Hus to boat from Aker Brygge
17:25 Departure of boat from Aker Brygge to Bygdøy. (Take bus 30 back/walking can be a pleasant alternative.)
18:30 Dinner

Thursday 13 June (HoTT-UF):

09:00 Liang Ze Wong: A Co-Reflection of Cubical Sets into Simplicial Sets
10:00 TYPES Pierre-Marie Pédrot and Nicolas Tabareau: Effects, Substitution and Induction: An Explosive Ménage à Trois
10:15 TYPES Malin Altenmüller and Conor McBride: Containers of Applications and Applications of Containers
10:30 Break
11:00 Taichi Uemura: Cubical Assembly Models of Homotopy Type Theory
12:00 TYPES Andreas Nuyts and Dominique Devriese: Menkar: Towards a Multimode Presheaf Proof Assistant
12:15 TYPES Marie Kerjean and Assia Mahboub: A formalisation of Hahn-Banach theorem in Coq
12:30 Lunch
14:00 Andrew Swan: Separating Path Types and Identity Types
15:00 TYPES Andreas Abel and Christian Sattler: Normalization by Evaluation for Call-by-Push-Value
15:15 TYPES Stefan Monnier and Nathaniel Bos: How Erasure is Linked to (im)Predicativity
15:30 Break
16:00 Paolo Capriotti: Globular Models of Type Theory

Friday 14 June (HoTT-UF):

09:00 Paige North: Directed weak factorization systems for type theory
10:00 TYPES Abhishek Dang and Piyush Kurur: Verse - An EDSL in Coq for verified low-level cryptographic primitives
10:15 TYPES Anton Setzer: A Model of the Blockchain using Induction-Recursion
10:30 Break
11:00 tslil clingman: Towards proof relevant category theory, as modelled by globular T-categories
12:00 TYPES Andreas Nuyts and Dominique Devriese: Dependable Atomicity in Type Theory
12:15 TYPES Niccolò Veltri and Niels van der Weide: Guarded Recursion in Agda via Sized Types
12:30 Lunch
14:00 Eric Finster: The Cotopological Tower
15:00 TYPES Robert Atkey and James Wood: Linear metatheory via linear algebra
15:15 TYPES Zhaohui Luo and Sergei Soloviev: Dependent Event Types in Event Semantics
15:30 Break
16:00 TYPES Venanzio Capretta and Colm Baston: Venanzio Capretta and Colm Baston
16:15 TYPES Fredrik Nordvall Forsberg: Compositional Game Theory using Dependent Types
16:30 Excursion to Holmenkollen (free). Bus to Holmenkollen leaves from Ingeniørenes Hus