Conference Programme

Program overview

 

18 June (Monday)

19 June (Tuesday)

20 June (Wednesday)

21 June (Thursday)
8:20-9:00
 registration + welcome      
9:00-10:00
 invited talk:        Josef Urban invited talk:        Delia Kesner invited talk: Matthieu Sozeau invited talk:      Cédric Fournet
10:00-10:40
 session 1 (2 talks): Meta-theory session 4 (2 talks): Co-induction session 6 (2 talks): Logic session 10 (2 talks): Partiality
10:40-11:10
 coffee break coffee break coffee break coffee break
11:10-12:30
 session 2 (4 talks): Applications session 5 (4 talks): Semantics session 7 (4 talks): Type theory session 11 (4 talks): Intersection types
12:30-14:20
 lunch lunch (until 14:00) lunch lunch
14:20-16:00
 session 3 (5 talks): HOTT and Univalence MC meeting of the COST Action EUTypes + TYPES business meeting (14:00-15:30) session 8 (4 talks): Tribute to Martin Hofmann session 12 (5 talks): Inductive types
16:00-16:30
 coffee break social programme (15:30-20:00) coffee break coffee break
16:30-18:10
 WG and dissemination meeting of Cost Action EUTypes session 9 (3 talks): Formalization  (until 17:30) session 13 (2 talks): Applications        (until 17:10)
 
20:00-
     conference dinner  

18 June (Monday)

8:20-8:50
 Registration
8:50-9:00
 Welcome
9:00-10:00
 Invited talk: Josef Urban
Title:  Machine Learning for Proof Automation and Formalization
10:00-10:20
 Session 1:          Meta-theory  (chair:  Herman Geuvers)
Andrej Dudenhefner and Jakob Rehof. A Simpler Undecidability Proof for System F Inhabitation
10:20-10:40
Beniamino Accattoli, Andrea Condoluci and Claudio Sacerdoti Coen. Sharing Equality is Linear
10:40-11:10
 Coffee break
11:10-11:30
 Session 2: Applications  (chair:  Aleksy Schubert)
Sergei Soloviev and Ian Malakhovsky. Automorphisms of Types for Security and Trust
11:30-11:50
 Ugo De Liguoro and Luca Padovani. Mailbox Types for Unordered Interactions
11:50-12:10
Luís Afonso Carvalho, João Costa Seco and Jácome Cunha. Typing the Evolution of Variational Software
12:10-12:30
Mirko Spasić and Milena Vujošević Janičić. First steps towards proving functional equivalence of embedded SQL
12:30-14:20
 Lunch break
14:20-14:40
 Session 3:     HOTT and  Univalence (chair:  Marc Bezem)
Taichi Uemura. Cubical Assemblies and Independence of the Propositional Resizing Axiom
14:40-15:00
Nicolai Kraus. On the Role of Semisimplicial Types
15:00-15:20
Paige North. A type theory for directed homotopy theory
15:20-15:40
Hugo Herbelin. Syntactic investigations into cubical type theory
15:40-16:00
Niels van der Weide, Dan Frumin and Herman Geuvers. 1-Types versus Groupoids
16:00-16:30
 Coffee break
16:30-18:10
 WG and dissemination meeting of Cost Action EUTypes  

 

 

19 June (Tuesday)

9:00-10:00
                                                              Invited talk:  Delia Kesner                                                         Title:  Multi Types for Higher-Order Languages
10:00-10:20
 Session 4:              Co-induction  (chair:  Ralph Matthes)
Anton Setzer. Simulating Codata Types using Coalgebras
10:20-10:40
Henning Basold. The Later Modality in Fibrations
10:40-11:10
 Coffee break
11:10-11:30

Session 5: Semantics  (chair: Tarmo Uustalu)

 
Valentin Blot and James Laird. Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types
11:30-11:50
Bassel Mannaa and Rasmus Møgelberg. The clocks they are adjunctions: Denotational semantics for Clocked Type Theory
11:50-12:10
Lars Birkedal, Ranald Clouston, Bassel Mannaa, Rasmus Ejlers Møgelberg, Andrew Pitts and Bas Spitters. Dependent Right Adjoint Types
12:10-12:30
Étienne Miquey. How delimited continuations can be used to define dependently typed CPS
12:30-14:00
 Lunch break
14:00-14:40
 MC meeting of the COST Action EUTypes
14:40-15:30
 TYPES business meeting
15:30-20:00
 Social programme

20 June (Wednesday)

9:00-10:00
 Invited talk:  Matthieu Sozeau
Title: The Predicative, Polymorphic Calculus of Cumulative Inductive Constructions and its implementation
10:00-10:20
 Session 6:         Logic  (chair:  Hugo Herbelin)
Silvia Ghilezan, Jelena Ivetic, Simona Kasterovic, Zoran Ognjanovic and Nenad Savic. Towards probabilistic reasoning about typed lambda terms
10:20-10:40
Herman Geuvers, Iris van der Giessen and Tonny Hurkens. Cut-elimination for general constructive proposition logic
10:40-11:10
 Coffee break
11:10-11:30
 Session 7:           Type theory  (chair:  Ambrus Kaposi)
András Kovács. Closure Conversion for Dependent Type Theory, With Type-Passing Polymorphism
11:30-11:50
Filippo Sestini. Towards Normalization for the Minimal Type Theory
11:50-12:10
Cesare Gallozzi. A Comparative Analysis of Type-Theoretic Interpretations of Constructive Set Theories
12:10-12:30
Zhaohui Luo. Formal Semantics in Modern Type Theories
12:30-14:20
 Lunch break
14:20-14:40
 Session 8:      Tribute to Martin Hofmann  (chair: Peter Dybjer) Invited talk: Ralph Matthes. Martin Hofmann’s case for non-strictly positive data types
14:40-15:00
 Théo Winterhalter, Matthieu Sozeau and Nicolas Tabareau. Using reflection to eliminate reflection
15:00-15:20
Steven Schäfer and Kathrin Stark. Embedding Higher-Order Abstract Syntax in Type Theory
15:20-15:40
Andreas Abel. Resourceful dependent types
15:40-16:00
Testimonies
16:00-16:30
 Coffee break
16:30-16:50
 Session 9: Formalization  (chair:  Frédéric Blanqui)
Benedikt Ahrens and Marco Maggesi. A modular formalization of bicategories in type theory
16:50-17:10
Ambroise Lafont, Tom Hirschowitz and Nicolas Tabareau. Types are weak omega-groupoids, in Coq
17:10-17:30
Paola Giannini, Tim Richter, Marco Servetto and Elena Zucca. Towards a mechanized soundness proof for sharing effects
17:30- TYPES business meeting (continuation)
 
20:00-
 Conference dinner

21 June (Thursday)

9:00-10:00
                                                         Invited talk:  Cédric Fournet                                                         Title:  Building verified cryptographic components using F*
10:00-10:20
 Session 10: Partiality  (chair: Andreas Abel)
Reinhard Kahle and Anton Setzer. Beyond the limits of the Curry-Howard isomorphism
10:20-10:40
Dominique Larchey-Wendling and Jean-François Monin. Simulating Induction-Recursion for Partial Algorithms
10:40-11:10
 Coffee break
11:10-11:30
 Session 11: Intersection types  (chair:  Jacob Rehof)
Davide Ancona, Giuseppe Castagna, Tommaso Petrucciani and Elena Zucca. Semantic subtyping for non-strict
languages
11:30-11:50
Pierre Vial. Typing every λ-term with infinitary non-idempotent types
11:50-12:10
Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani and Jeremy Siek. Polymorphic Gradual Typing: A Set-Theoretic Perspective
12:10-12:30
Luigi Liquori and Claude Stolze. Characterization of eight intersection type systems à la Church
12:30-14:20
 Lunch break
14:20-14:40
 Session 12: Inductive types  (chair:  Ana Bove)
Jesper Cockx, Gaëtan Gilbert and Nicolas Tabareau. Vectors are records, too
14:40-15:00
Thorsten Altenkirch, Ambrus Kaposi, András Kovács and Jakob von Raumer. Reducing Inductive-Inductive Types to Indexed Inductive Types
15:00-15:20
Gun Pinyo and Thorsten Altenkirch. Integers as a Higher Inductive Type
15:20-15:40
Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus and Fredrik Nordvall Forsberg. Specifying Quotient Inductive-Inductive Types
15:40-16:00
Thorsten Altenkirch, Péter Diviánszky, Ambrus Kaposi and András Kovács. Constructing inductive-inductive types using a domain-specific type theory
16:00-16:30
 Coffee break
16:30-16:50
 Session 13: Applications  (chair:  Ugo de’Liguoro)
Vasco T. Vasconcelos, Antónia Lopes and Francisco Martins. HeadREST: A Specification Language for RESTful APIs
16:50-17:10
Tõnn Talvik and Tarmo Uustalu. Experimenting with graded monads: certified grading-based program transformations