The TYPES meeting will run from Monday June 20th to Thursday June 23th, followed by EuroProofNet meetings on June 24th and June 25th.
Programme
This is a tentative programme that may be still subject to change without notice.
Monday
Monday 9:00-10:00
- Invited Talk: On the expressive power of types (Sam Lindley)
Monday 10:00-10:30
- Short Talk: Partial Dijkstra Monads for All (Théo Winterhalter, Cezar-Constantin Andrici, Catalin Hritcu, Kenji Maillard, Guido Martínez and Exequiel Rivas)
- Short Talk: Flexible presentations of graded monads (Shin-Ya Katsumata, Dylan McDermott, Tarmo Uustalu and Nicolas Wu)
Monday 10:50-12:30
- Long Talk: BioTT: a Family of Brouwerian Intuitionistic Theories Open to Classical Reasoning (Mark Bickford, Liron Cohen, Robert Constable and Vincent Rahli)
- Short Talk: Towards Higher Observational Type Theory (Thorsten Altenkirch, Ambrus Kaposi and Mike Shulman)
- Short Talk: Two Guarded Recursive Powerdomains for Applicative Simulation (Rasmus Ejlers Møgelberg and Andrea Vezzosi)
- Short Talk: Noninvasive Polarized Subtyping for Inductive Types (Théo Laurent and Kenji Maillard)
- Short Talk: Extending truth table natural deduction to predicate logic (Herman Geuvers and Tonny Hurkens)
- Short Talk: Interpreting second-order arithmetic via update recursion (Valentin Blot)
Monday 14:00-15:55
- Long Talk: A Theory of Call-by-Value Solvability (Beniamino Accattoli and Giulio Guerrieri)
- Short Talk: Quantitative Perspectives on Generalized Applications (Loïc Peyrot)
- Short Talk: Quantitative Inhabitation in Call-by-Value (Victor Arrial)
- Short Talk: Linear Rank Intersection Types (Fábio Reis, Sandra Alves and Mário Florido)
- Short Talk: Realizing Implicit Computational Complexity (Clément Aubert, Thomas Rubiano, Neea Rusch and Thomas Seiller)
- Short Talk: Towards Probabilistic Reasoning about Typed Combinatory Terms (Simona Kašterović and Silvia Ghilezan)
- Short Talk: Proof-relevant normalization for intersection types with profunctors (Zeinab Galal)
Monday 16:30-17:55
- Long Talk: Type Theories with Universe Level Judgments (Marc Bezem, Thierry Coquand, Peter Dybjer and Martín Escardó)
- Short Talk: Extending Cubical Agda with Internal Parametricity (Antoine Van Muylder, Andrea Vezzosi, Andreas Nuyts and Dominique Devriese)
- Short Talk: From iterated parametricity to indexed semi-cubical and semi-simplicial sets: a formal construction (Hugo Herbelin and Ramkumar Ramachandra)
- Short Talk: Deciding the cofibration logic of cartesian cubical type theories (Robert Rose, Matthew Weaver and Daniel Licata)
- Short Talk: Cubical models are cofreely parametric (Hugo Moeneclaey)
Tuesday
Tuesday 9:00-10:25
- Long Talk: An Agda Formalisation of Modalities and Erasure in a Dependently Typed Language (Oskar Eriksson and Andreas Abel)
- Short Talk: Sikkel: Multimode Simple Type Theory as an Agda Library (Joris Ceulemans, Andreas Nuyts and Dominique Devriese)
- Short Talk: Unifying Cubical and Multimodal Type Theory (Frederik L. Aagaard, Magnus B. Kristensen, Daniel Gratzer and Lars Birkedal)
- Short Talk: Transpension: The Right Adjoint to the Pi-Type (Andreas Nuyts and Dominique Devriese)
- Short Talk: Conservativity of Two-Level Type Theory Corresponds to Staged Compilation (András Kovács)
Tuesday 10:50-12:25
- Long Talk: Session Type Systems Compared: The Case of Deadlock Freedom (Ornela Dardha and Jorge A. Pérez)
- Short Talk: A Simple Concurrent Lambda Calculus for Encoding Session types (Jules Jacobs)
- Long Talk: On Dynamic Lifting and Effect Typing in Circuit Description Languages (Andrea Colledan and Ugo Dal Lago)
- Short Talk: Capable GV: Capabilities for Session Types in GV (Magdalena J. Latifa and Ornela Dardha)
- Short Talk: Linear lambda-calculus is linear (Alejandro Díaz-Caro and Gilles Dowek)
Tuesday 14:00-16:00
- Short Talk: The 4th Homotopy Group of the 3-Sphere in Cubical Agda (Axel Ljungström and Anders Mörtberg)
- Short Talk: Pre-bilattices in Univalent Foundations (Georgios V. Pitsiladis)
- Short Talk: Displayed Monoidal Categories (Benedikt Ahrens, Ralph Matthes and Kobe Wullaert)
- Short Talk: Implementing Martin-Löf’s meaning explanations for intuitionistic type theory in Agda (Peter Dybjer and Anton Setzer)
- Short Talk: Towards a Mechanized Theory of Computation for Education (Tiago Cogumbreiro and Yannick Forster)
- Short Talk: Myhill Isomorphism Theorem and a Computational Cantor-Bernstein Theorem in Constructive Type Theory (Yannick Forster, Felix Jahn and Gert Smolka)
- Short Talk: Toward a denotational semantics of streams for a verified Lustre compiler (Paul Jeanmaire, Timothy Bourke and Marc Pouzet)
- Short Talk: Synthetic Turing Reducibility in CIC (Yannick Forster and Dominik Kirst)
Tuesday 16:30-17:30
- Invited Talk: The Lean 4 theorem prover and programming language (Leonardo De Moura)
Tuesday 18:00-19:00
- Business Meeting
Wednesday
Wednesday 9:00-10:00
- Invited Talk: Composing Music from Types (Youyou Cong)
Wednesday 10:00-10:25
- Long Talk: Strong, Synthetic, and Computational Proofs of Gödel’s First Incompleteness Theorem (Benjamin Peters and Dominik Kirst)
Wednesday 10:50-12:20
- Long Talk: TypOS: An Operating System for Typechecking Actors (Guillaume Allais, Malin Altenmüller, Conor Mcbride, Georgi Nakov, Fredrik Nordvall Forsberg and Craig Roy)
- Short Talk: A Flexible Multimodal Proof Assistant (Philipp Stassen, Daniel Gratzer and Lars Birkedal)
- Short Talk: Type Inference via Symbolic Environment Transformations (Ulrich Schöpp and Chuangjie Xu)
- Short Talk: Aspects of a machine-checked intermediate language for extraction from Coq, in MetaCoq (Yannick Forster and Matthieu Sozeau)
- Short Talk: Verification Techniques for Smart Contracts in Agda (Fahad Alhabardi, Arnold Beckmann, Bogdan Lazar and Anton Setzer)
- Short Talk: Exhaustive testing of property testers (Auke Booij)
Wednesday 14:00-14:55
- Long Talk: A Generalized Translation of Pure Type Systems (Nathan Mull)
- Short Talk: Killing Two Hens with One Stone – Equivalence Between Typed and Untyped Algorithmic Conversions (Meven Lennon-Bertrand)
- Short Talk: Canonicity and decidability of equality for setoid type theory (István Donkó and Ambrus Kaposi)
Wednesday 16:00-18:00
- Social event: Machines de l’Île (more information here)
Wednesday 20:00
- Social diner at Le 1
Thursday
Thursday 9:00-10:00
- Invited Talk: Refine and Synthesise: a type-theoretic view on neural network robustness (Ekaterina Komendantskaya)
Thursday 10:00-10:25
- Long Talk: The Münchhausen method and combinatory type theory (Thorsten Altenkirch, Ambrus Kaposi, Artjoms Šinkarovs and Tamás Végh)
Thursday 10:50-12:30
- Long Talk: Resizing Prop down to an axiom (Stefan Monnier)
- Short Talk: Towards a Formalization of Affine Schemes in Cubical Agda (Anders Mörtberg and Max Zeuner)
- Short Talk: Higher-Order Universe Operators in Martin-Löf Type Theory with one Mahlo Universe (Yuta Takahashi)
- Short Talk: A Reasonably Gradual Type Theory (Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau and Éric Tanter)
- Short Talk: Semantics for two-dimensional type theory (Benedikt Ahrens, Paige North and Niels van der Weide)
- Short Talk: Synthetic Versions of the Kleene-Post and Post’s Theorem (Dominik Kirst, Niklas Mück and Yannick Forster)
Thursday 14:00-15:50
- Long Talk: A Datatype of Planar Graphs (Malin Altenmüller and Conor McBride)
- Short Talk: Monsters: Programming and Reasoning (Venanzio Capretta and Christopher Purdy)
- Short Talk: Data Types with Negation (Robert Atkey)
- Short Talk: Consistent Ultrafinitist Logic (Michal Gajda)
- Long Talk: Decidability and Semidecidability via ordinals (Nicolai Kraus, Fredrik Nordvall Forsberg and Chuangjie Xu)
- Short Talk: The Patch Frame of a Spectral Locale in Univalent Type Theory (Ayberk Tosun and Martín Escardó)
Thursday 16:30-17:55
- Long Talk: More on modal embeddings and calling paradigms (José Espírito Santo, Luís Pinto and Tarmo Uustalu)
- Short Talk: Certified Abstract Machines for Skeletal Semantics (Guillaume Ambal, Sergueï Lenglet and Alan Schmitt)
- Short Talk: Towards a translation from K to Dedukti (Amélie Ledein, Valentin Blot and Catherine Dubois)
- Short Talk: Validating OCaml soundness by translation into Coq (Jacques Garrigue and Takafumi Saikawa)
- Short Talk: Small inversions for smaller inversions (Jean-Francois Monin)
Pre-recorded talks
- Pre-recorded talk: Forwarders as Process Compatibility, Logically (Marco Carbone, Sonia Marin and Carsten Schuermann)
- Pre-recorded talk: Description Operators in Partial Propositional Type Theory (Víctor Aranda and Manuel Martins)
- Pre-recorded talk: A Domain-Specific Language for Name Modifiers (Kuen-Bang Hou Favonia)
- Pre-recorded talk: Synthetic Tait Computability for Simplicial Type Theory (Jonathan Weinberger, Benedikt Ahrens, Ulrik Buchholtz and Paige North)
- Pre-recorded talk: Homotopy setoids and quotient completion (Cipriano Cioffo)
Accepted Papers
- A Datatype of Planar Graphs (Malin Altenmüller and Conor McBride)
- A Domain-Specific Language for Name Modifiers (Kuen-Bang Hou Favonia)
- A Flexible Multimodal Proof Assistant (Philipp Stassen, Daniel Gratzer and Lars Birkedal)
- A Generalized Translation of Pure Type Systems (Nathan Mull)
- A Reasonably Gradual Type Theory (Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau and Éric Tanter)
- A Simple Concurrent Lambda Calculus for Encoding Session types (Jules Jacobs)
- A Theory of Call-by-Value Solvability (Beniamino Accattoli and Giulio Guerrieri)
- An Agda Formalisation of Modalities and Erasure in a Dependently Typed Language (Oskar Eriksson and Andreas Abel)
- Aspects of a machine-checked intermediate language for extraction from Coq, in MetaCoq (Yannick Forster and Matthieu Sozeau)
- BioTT: a Family of Brouwerian Intuitionistic Theories Open to Classical Reasoning (Mark Bickford, Liron Cohen, Robert Constable and Vincent Rahli)
- Canonicity and decidability of equality for setoid type theory (István Donkó and Ambrus Kaposi)
- Capable GV: Capabilities for Session Types in GV (Magdalena J. Latifa and Ornela Dardha)
- Certified Abstract Machines for Skeletal Semantics (Guillaume Ambal, Sergueï Lenglet and Alan Schmitt)
- Conservativity of Two-Level Type Theory Corresponds to Staged Compilation (András Kovács)
- Consistent Ultrafinitist Logic (Michal Gajda)
- Cubical models are cofreely parametric (Hugo Moeneclaey)
- Data Types with Negation (Robert Atkey)
- Decidability and Semidecidability via ordinals (Nicolai Kraus, Fredrik Nordvall Forsberg and Chuangjie Xu)
- Deciding the cofibration logic of cartesian cubical type theories (Robert Rose, Matthew Weaver and Daniel Licata)
- Description Operators in Partial Propositional Type Theory (Víctor Aranda and Manuel Martins)
- Displayed Monoidal Categories (Benedikt Ahrens, Ralph Matthes and Kobe Wullaert)
- Exhaustive testing of property testers (Auke Booij)
- Extending Cubical Agda with Internal Parametricity (Antoine Van Muylder, Andrea Vezzosi, Andreas Nuyts and Dominique Devriese)
- Extending truth table natural deduction to predicate logic (Herman Geuvers and Tonny Hurkens)
- Flexible presentations of graded monads (Shin-Ya Katsumata, Dylan McDermott, Tarmo Uustalu and Nicolas Wu)
- Forwarders as Process Compatibility, Logically (Marco Carbone, Sonia Marin and Carsten Schuermann)
- From iterated parametricity to indexed semi-cubical and semi-simplicial sets: a formal construction (Hugo Herbelin and Ramkumar Ramachandra)
- Higher-Order Universe Operators in Martin-Löf Type Theory with one Mahlo Universe (Yuta Takahashi)
- Homotopy setoids and quotient completion (Cipriano Cioffo)
- Implementing Martin-Löf’s meaning explanations for intuitionistic type theory in Agda (Peter Dybjer and Anton Setzer)
- Interpreting second-order arithmetic via update recursion (Valentin Blot)
- Killing Two Hens with One Stone – Equivalence Between Typed and Untyped Algorithmic Conversions (Meven Lennon-Bertrand)
- Linear lambda-calculus is linear (Alejandro Díaz-Caro and Gilles Dowek)
- Linear Rank Intersection Types (Fábio Reis, Sandra Alves and Mário Florido)
- Monsters: Programming and Reasoning (Venanzio Capretta and Christopher Purdy)
- More on modal embeddings and calling paradigms (José Espírito Santo, Luís Pinto and Tarmo Uustalu)
- Myhill Isomorphism Theorem and a Computational Cantor-Bernstein Theorem in Constructive Type Theory (Yannick Forster, Felix Jahn and Gert Smolka)
- Noninvasive Polarized Subtyping for Inductive Types (Théo Laurent and Kenji Maillard)
- On Dynamic Lifting and Effect Typing in Circuit Description Languages (Andrea Colledan and Ugo Dal Lago)
- Partial Dijkstra Monads for All (Théo Winterhalter, Cezar-Constantin Andrici, Catalin Hritcu, Kenji Maillard, Guido Martínez and Exequiel Rivas)
- Pre-bilattices in Univalent Foundations (Georgios V. Pitsiladis)
- Proof-relevant normalization for intersection types with profunctors (Zeinab Galal)
- Quantitative Inhabitation in Call-by-Value (Victor Arrial)
- Quantitative Perspectives on Generalized Applications (Loïc Peyrot)
- Realizing Implicit Computational Complexity (Clément Aubert, Thomas Rubiano, Neea Rusch and Thomas Seiller)
- Resizing Prop down to an axiom (Stefan Monnier)
- Semantics for two-dimensional type theory (Benedikt Ahrens, Paige North and Niels van der Weide)
- Session Type Systems Compared: The Case of Deadlock Freedom (Ornela Dardha and Jorge A. Pérez)
- Sikkel: Multimode Simple Type Theory as an Agda Library (Joris Ceulemans, Andreas Nuyts and Dominique Devriese)
- Small inversions for smaller inversions (Jean-Francois Monin)
- Strong, Synthetic, and Computational Proofs of Gödel’s First Incompleteness Theorem (Benjamin Peters and Dominik Kirst)
- Synthetic Tait Computability for Simplicial Type Theory (Jonathan Weinberger, Benedikt Ahrens, Ulrik Buchholtz and Paige North)
- Synthetic Turing Reducibility in CIC (Yannick Forster and Dominik Kirst)
- Synthetic Versions of the Kleene-Post and Post’s Theorem (Dominik Kirst, Niklas Mück and Yannick Forster)
- The 4th Homotopy Group of the 3-Sphere in Cubical Agda (Axel Ljungström and Anders Mörtberg)
- The Münchhausen method and combinatory type theory (Thorsten Altenkirch, Ambrus Kaposi, Artjoms Šinkarovs and Tamás Végh)
- The Patch Frame of a Spectral Locale in Univalent Type Theory (Ayberk Tosun and Martín Escardó)
- Toward a denotational semantics of streams for a verified Lustre compiler (Paul Jeanmaire, Timothy Bourke and Marc Pouzet)
- Towards a Formalization of Affine Schemes in Cubical Agda (Anders Mörtberg and Max Zeuner)
- Towards a Mechanized Theory of Computation for Education (Tiago Cogumbreiro and Yannick Forster)
- Towards a translation from K to Dedukti (Amélie Ledein, Valentin Blot and Catherine Dubois)
- Towards Higher Observational Type Theory (Thorsten Altenkirch, Ambrus Kaposi and Mike Shulman)
- Towards Probabilistic Reasoning about Typed Combinatory Terms (Simona Kašterović and Silvia Ghilezan)
- Transpension: The Right Adjoint to the Pi-Type (Andreas Nuyts and Dominique Devriese)
- Two Guarded Recursive Powerdomains for Applicative Simulation (Rasmus Ejlers Møgelberg and Andrea Vezzosi)
- Type Inference via Symbolic Environment Transformations (Ulrich Schöpp and Chuangjie Xu)
- Type Theories with Universe Level Judgments (Marc Bezem, Thierry Coquand, Peter Dybjer and Martín Escardó)
- TypOS: An Operating System for Typechecking Actors (Guillaume Allais, Malin Altenmüller, Conor Mcbride, Georgi Nakov, Fredrik Nordvall Forsberg and Craig Roy)
- Unifying Cubical and Multimodal Type Theory (Frederik L. Aagaard, Magnus B. Kristensen, Daniel Gratzer and Lars Birkedal)
- Validating OCaml soundness by translation into Coq (Jacques Garrigue and Takafumi Saikawa)
- Verification Techniques for Smart Contracts in Agda (Fahad Alhabardi, Arnold Beckmann, Bogdan Lazar and Anton Setzer)