Program (draft)

Program overview

18 June (Monday)

19 June (Tuesday)

20 June (Wednesday)

21 June (Thursday)

8:30-9:00
registration
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 + business meetings (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 + dissemination meetings session 9 (5 talks): Formalization session 13 (2 talks):  Applications  (until 17:10)
20:00-
conference diner

18 June (Monday)

8:30-9:00
Registration
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: )
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: )
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
Bogdan Aman and Gabriel Ciobanu. Session Types for Timed Migration
12:30-14:20
Lunch break
14:20-14:40
Session 3:          HOTT and Univalence      (chair: )
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 + Dissemination meetings​

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: )
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: )
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-15:30
MC meeting + Business meetings
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: )
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: )
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: )
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-17:50
Sophie Bernard. A Constructive Morphism between Algebraic Fields and (Real-)Closed Fields
17:50-18:10
Tõnn Talvik and Tarmo Uustalu. Experimenting with graded monads: certified grading-based program transformations
20:00-
Conference diner

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: )
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: )
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: )
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: )
Mirko Spasić and Milena Vujošević Janičić. First steps towards proving functional equivalence of embedded SQL
16:50-17:10
Vasco T. Vasconcelos, Antónia Lopes and Francisco Martins. HeadREST: A Specification Language for RESTful APIs