9:00 Registration
9:25-9:30 Workshop opening by Marc Bezem
Session 1 Curry-Howard
9:30-10:00 Extended Curry-Howard Correspondence: The Case of Loeb Logic Tadeusz Litak
10:00-10:30 On the Curry-Howard Correspondence for Constructive Modal Logic CK Michael Mendler
10:30-11:00 Coffee Break
Session 2 Logics
11:00-11:30 Model Theory of Logic-Enriched Type Theories Robin Adams
11:30-12:00 Extension of General Logic Patrik Eklund and Robert Helgesson
12:00-12:30 Decision Problems in Intersection Logics Pawel Urzyczyn
12:30-14:00 Lunch Break
Session 3 Category Theory
14:00-14:30 Algebraic Foundations for Type Theories Marcelo Fiore
14:30-15:00 Computing in a Boolean Topos Arnaud Spiwack
15:00-15:30 Abstract Structural Induction Robert Atkey, Patricia Johann and Neil Ghani
15:30-16:00 Coffee Break
Session 4 Induction
16:00-16:30 A Monoidal Category of Inductive Recursive Definitions Neil Ghani, Peter Hancock, Conor Mcbride and Lorenzo Malatesta
16:30-17:00 An Equivalence between Small Induction Recursion and Indexed Containers Lorenzo Malatesta, Thorsten Altenkirch, Neil Ghani, Peter Hancock and Conor Mcbride
17:00-17:30 Elimination Principles for Initial Dialgebras Fredrik Nordvall Forsberg, Thorsten Altenkirch, Peter Morris and Anton Setzer
Session 5 Invited Talk
9:00-10:00 Type Design Patterns for Computer Proofs Georges Gonthier, Cambridge
10:00-10:30 Coffee Break
Session 6
10:30-11:00 Ornaments: Organising the Zoo of Data-types Pierre-Evariste Dagand and Conor Mcbride
11:00-11:30 Logical Predicates as First-Class Citizens in LF Furio Honsell, Marina Lenisa, Luigi Liquori, Petar Maksimovic and Ivan Scagnetto
11:30-12:00 A User-extensible and Safe Alternative to the Conversion Rule using VeriML Antonis Stampoulis and Zhong Shao
12:00-12:30 Context-dependent Computation using Comodels of Theories in Type Theory Tarmo Uustalu
12:30-14:00 Lunch Break
Session 7 Formalised Mathematics/Arithmetics/Geometry
14:00-14:30 Certified Polynomial Approximation for Solving the Table Maker's Dilemma Nicolas Brisebarre, Mioara Joldes, Erik Martin-Dorel, Micaela Mayero, Jean-Michel Muller, Ioana Pasca, Laurence Rideau and Laurent Théry
14:30-15:00 Real Algebraic Geometry: A Formalization of a Quantifier Elimination Procedure for the Theory of Real Closed Field Cyril Cohen and Assia Mahboubi
15:00-15:30 Formalizing a Discrete Model of the Continuum in Coq from a Discrete Geometry Perspective Nicolas Magaud, Agathe Chollet and Laurent Fuchs
15:30-16:00 Coffee Break
Session 8 Constructive Mathematics/Algebra
16:00-16:30 Infinite Sets that Satisfy the Principle of Omniscience in all Varieties of Constructive Mathematics Martin Escardo
16:30-17:00 Type Classes for Efficient Exact Real Arithmetic in Coq Robbert Krebbers and Bas Spitters
17:00-17:30 Rings with Explicit Divisibility Formalized in Coq Anders Mörtberg and Cyril Cohen
17:30 TYPES business meeting (agenda: next workshop, post-proceedings, ...)
Session 9 Invited Talk
9:00-10:00 Sequential versus Continuous Models of Finite Types Dag Normann, Oslo
10:00-10:30 Coffee Break
Session 10 Typing and Subtyping
10:30-11:00 Comparative Study of Different Styles of Coinductive Logic Programming for Type Inference Ekaterina Komendantskaya
11:00-11:30 Mechanizing Metatheory without Typing Contexts Sungwoo Park
11:30-12:00 The Principal Subtyping Theorem and the Subtyping Hierarchy of Lambda Terms Andrew Polonsky
12:00-12:30 Type-Theoretical Semantics with Coercive Subtyping Zhaohui Luo
12:30-14:00 Lunch Break
Session 11 Type Systems
14:00-14:30 A Type System for Positivity Matteo Acerbi, Dominic Mulligan and Claudio Sacerdoti Coen
14:30-15:00 The Role of Second-order Quantification in Soft Type Assignment Systems Aleksy Schubert, Jacek Chrząszcz and Ken-Etsu Fujita
15:00-15:30 PTS with Typed Equality and Explicit Substitutions Daniel Fridlender and Miguel Pagano
15:30-15:45 Coffee Break (short)
Session 12 Type Systems/Lambda Calculus
15:45-16:15 On Vectorial Typing Alejandro Díaz-Caro
16:15-16:45 Exploring the Reach of Hereditary Substitution Harley D. Eades III and Aaron Stump
16:45-17:15 A Characterization of Reduction 1-Cycles in Infinitary Lambda Calculus Andrew Polonsky and Jörg Endrullis
Workshop Dinner
17:30 Walk to Dreggekaien on Bryggen, boat to Cornelius restaurant leaves 18:00 (sharp)
Session 13 Invited Talk
9:30-10:30 Resizing rules - their use and semantic justification Vladimir Voevodsky, Princeton
10:30-11:00 Coffee Break
Session 14
11:00-11:30 Formal Proofs of Robustness for Watermarking Algorithms David Baelde, Pierre Courtieu, David Gross-Amblard, Christine Paulin and Xavier Urbain
11:30-12:00 Prototype Implementation of an Inhabitation Algorithm for FCL$(\cap, \leq)$ Boris Duedder, Moritz Martens and Jakob Rehof
12:00-12:30 Economic Equilibriai in Type Theory Cezar Ionescu
12:30-14:00 Lunch Break
Session 15
14:00-14:30 Initiality for Typed Syntax and Semantics Benedikt Ahrens
14:30-15:00 The Link between the Intensional Level and the Extensional one in the Minimalist Foundation Maria Emilia Maietti
15:00-15:30 Towards a Computational Justification of the Axiom of Univalence Simon Huber and Thierry Coquand
15:30-16:00 A Computational Proof of Dependent Choice Compatible with Classical Logic Hugo Herbelin
16:00-16:30 Coffee Break
Excursion
16:30-22:00 Excursion (hike with meal on Ulriken)