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: ) |
A Simpler Undecidability Proof for System F Inhabitation
|
10:20-10:40 |
Sharing Equality is Linear
|
|
10:40-11:10 |
Coffee break | |
11:10-11:30 |
Session 2: Applications (chair: ) |
Automorphisms of Types for Security and Trust
|
11:30-11:50 |
Mailbox Types for Unordered Interactions | |
11:50-12:10 |
Typing the Evolution of Variational Software
|
|
12:10-12:30 |
Session Types for Timed Migration
|
|
12:30-14:20 |
Lunch break | |
14:20-14:40 |
Session 3: HOTT and Univalence (chair: ) |
Cubical Assemblies and Independence of the Propositional Resizing Axiom
|
14:40-15:00 |
On the Role of Semisimplicial Types
|
|
15:00-15:20 |
A type theory for directed homotopy theory
|
|
15:20-15:40 |
Syntactic investigations into cubical type theory
|
|
15:40-16:00 |
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: ) |
Simulating Codata Types using Coalgebras
|
10:20-10:40 |
The Later Modality in Fibrations
|
|
10:40-11:10 |
Coffee break | |
11:10-11:30 |
Session 5: Semantics (chair: ) |
Extensional and Intensional Semantic Universes: A Denotational Model of Dependent Types
|
11:30-11:50 |
The clocks they are adjunctions: Denotational semantics for Clocked Type Theory
|
|
11:50-12:10 |
Dependent Right Adjoint Types
|
|
12:10-12:30 |
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: ) |
Towards probabilistic reasoning about typed lambda terms
|
10:20-10:40 |
Cut-elimination for general constructive proposition logic
|
|
10:40-11:10 |
Coffee break | |
11:10-11:30 |
Session 7: Type theory (chair: ) |
Closure Conversion for Dependent Type Theory, With Type-Passing Polymorphism
|
11:30-11:50 |
Towards Normalization for the Minimal Type Theory
|
|
11:50-12:10 |
A Comparative Analysis of Type-Theoretic Interpretations of Constructive Set Theories
|
|
12:10-12:30 |
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) | Martin Hofmann’s case for non-strictly positive data types |
14:40-15:00 |
Using reflection to eliminate reflection | |
15:00-15:20 |
Embedding Higher-Order Abstract Syntax in Type Theory
|
|
15:20-15:40 |
Resourceful dependent types
|
|
15:40-16:00 |
Testimonies
|
|
16:00-16:30 |
Coffee break | |
16:30-16:50 |
Session 9: Formalization (chair: ) |
A modular formalization of bicategories in type theory
|
16:50-17:10 |
Types are weak omega-groupoids, in Coq
|
|
17:10-17:30 |
Towards a mechanized soundness proof for sharing effects
|
|
17:30-17:50 |
A Constructive Morphism between Algebraic Fields and (Real-)Closed Fields
|
|
17:50-18:10 |
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: ) |
Beyond the limits of the Curry-Howard isomorphism
|
10:20-10:40 |
Simulating Induction-Recursion for Partial Algorithms
|
|
10:40-11:10 |
Coffee break | |
11:10-11:30 |
Session 11: Intersection types (chair: ) |
Semantic subtyping for non-strict languages
|
11:30-11:50 |
Typing every λ-term with infinitary non-idempotent types
|
|
11:50-12:10 |
Polymorphic Gradual Typing: A Set-Theoretic Perspective
|
|
12:10-12:30 |
Characterization of eight intersection type systems à la Church
|
|
12:30-14:20 |
Lunch break | |
14:20-14:40 |
Session 12: Inductive types (chair: ) |
Vectors are records, too
|
14:40-15:00 |
Reducing Inductive-Inductive Types to Indexed Inductive Types
|
|
15:00-15:20 |
Integers as a Higher Inductive Type
|
|
15:20-15:40 |
Specifying Quotient Inductive-Inductive Types
|
|
15:40-16:00 |
Constructing inductive-inductive types using a domain-specific type theory
|
|
16:00-16:30 |
Coffee break | |
16:30-16:50 |
Session 13: Applications (chair: ) |
First steps towards proving functional equivalence of embedded SQL
|
16:50-17:10 |
HeadREST: A Specification Language for RESTful APIs
|
|