Programme

The TYPES meeting will run from Monday June 20th to Thursday June 23th, followed by EuroProofNet meetings on June 24th and June 25th.

The list of abstracts can be downloaded as a single file through the following link. Otherwise, each abstract is available as a standalone file by clicking on the corresponding title in the programme.

Programme

The TYPES programme follows the following conventions.

• Invited talks are one hour long, including questions.
• Short talks are 10 minute long + 5 minutes for questions.
• Long talks are 20 minute long + 5 minutes for questions.

Monday

Monday 9:00-10:30 (Chair: Éric Tanter)

• Invited Talk: On the expressive power of types [slides] (Sam Lindley)
• Short Talk: Partial Dijkstra Monads for All [slides] (Théo Winterhalter, Cezar-Constantin Andrici, Catalin Hritcu, Kenji Maillard, Guido Martínez and Exequiel Rivas)
• Short Talk: Flexible presentations of graded monads [slides] (Shin-Ya Katsumata, Dylan McDermott, Tarmo Uustalu and Nicolas Wu)

Monday 10:30-10:50

• Break

Monday 10:50-12:30 (Chair: Pierre-Marie Pédrot)

• Long Talk: BioTT: a Family of Brouwerian Intuitionistic Theories Open to Classical Reasoning [slides] (Mark Bickford, Liron Cohen, Robert Constable and Vincent Rahli)
• Short Talk: Towards Higher Observational Type Theory [slides] (Thorsten Altenkirch, Ambrus Kaposi and Mike Shulman)
• Short Talk: Two Guarded Recursive Powerdomains for Applicative Simulation [slides] (Rasmus Ejlers Møgelberg and Andrea Vezzosi)
• Short Talk: Noninvasive Polarized Subtyping for Inductive Types [slides] (Théo Laurent and Kenji Maillard)
• Short Talk: Extending truth table natural deduction to predicate logic [slides] (Herman Geuvers and Tonny Hurkens)
• Short Talk: Interpreting second-order arithmetic via update recursion [slides] (Valentin Blot)

Monday 12:30-14:00

• Lunch

Monday 14:00-15:55 (Chair: Lionel Vaux Auclair)

• Long Talk: A Theory of Call-by-Value Solvability [slides] (Beniamino Accattoli and Giulio Guerrieri)
• Short Talk: Quantitative Perspectives on Generalized Applications [slides] (Loïc Peyrot)
• Short Talk: Quantitative Inhabitation in Call-by-Value (Victor Arrial)
• Short Talk: Linear Rank Intersection Types [slides] (Fábio Reis, Sandra Alves and Mário Florido)
• Short Talk: Realizing Implicit Computational Complexity [slides] (Clément Aubert, Thomas Rubiano, Neea Rusch and Thomas Seiller)
• Short Talk: Towards Probabilistic Reasoning about Typed Combinatory Terms [slides] (Simona Kašterović and Silvia Ghilezan)
• Short Talk: Proof-relevant normalization for intersection types with profunctors [slides] (Zeinab Galal)

Monday 15:55-16:30

• Break

Monday 16:30-17:55 (Chair: Thierry Coquand)

• Long Talk: Type Theories with Universe Level Judgments [slides] (Marc Bezem, Thierry Coquand, Peter Dybjer and Martín Escardó)
• Short Talk: Extending Cubical Agda with Internal Parametricity [slides] (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 [slides] (Hugo Herbelin and Ramkumar Ramachandra)
• Short Talk: Deciding the cofibration logic of cartesian cubical type theories [slides] (Robert Rose, Matthew Weaver and Daniel Licata)
• Short Talk: Cubical models are cofreely parametric [slides] (Hugo Moeneclaey)

Monday 18:30-…

• Social event: Welcome Drinks & Pizza at LumberJack Petit Port (walking distance from the venue)

Tuesday

Tuesday 9:00-10:25 (Chair: Anton Setzer)

• 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 [slides] (Joris Ceulemans, Andreas Nuyts and Dominique Devriese)
• Short Talk: Unifying Cubical and Multimodal Type Theory [slides] (Frederik L. Aagaard, Magnus B. Kristensen, Daniel Gratzer and Lars Birkedal)
• Short Talk: Transpension: The Right Adjoint to the Pi-Type [slides] (Andreas Nuyts and Dominique Devriese)
• Short Talk: Conservativity of Two-Level Type Theory Corresponds to Staged Compilation [slides] (András Kovács)

Tuesday 10:25-10:50

• Break

Tuesday 10:50-12:25 (Chair: Delia Kesner)

• Long Talk: Session Type Systems Compared: The Case of Deadlock Freedom [slides] (Ornela Dardha and Jorge A. Pérez)
• Short Talk: A Simple Concurrent Lambda Calculus for Encoding Session types [slides] (Jules Jacobs)
• Long Talk: On Dynamic Lifting and Effect Typing in Circuit Description Languages [slides] (Andrea Colledan and Ugo Dal Lago)
• Short Talk: Capable GV: Capabilities for Session Types in GV [slides] (Magdalena J. Latifa and Ornela Dardha)
• Short Talk: Linear lambda-calculus is linear [slides] (Alejandro Díaz-Caro and Gilles Dowek)

Tuesday 12:25-14:00

• Lunch

Tuesday 14:00-16:00 (Chair: András Kovács)

• 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 [slides] (Georgios V. Pitsiladis)
• Short Talk: Case Study on Displayed Monoidal Categories [slides] (Benedikt Ahrens, Ralph Matthes and Kobe Wullaert)
• Short Talk: Implementing Martin-Löf’s meaning explanations for intuitionistic type theory in Agda [slides] (Peter Dybjer and Anton Setzer)
• Short Talk: Towards a Mechanized Theory of Computation for Education [slides] (Tiago Cogumbreiro and Yannick Forster)
• Short Talk: Myhill Isomorphism Theorem and a Computational Cantor-Bernstein Theorem in Constructive Type Theory [slides] (Yannick Forster, Felix Jahn and Gert Smolka)
• Short Talk: Toward a denotational semantics of streams for a verified Lustre compiler [slides] (Paul Jeanmaire, Timothy Bourke and Marc Pouzet)
• Short Talk: Synthetic Turing Reducibility in CIC [slides] (Yannick Forster and Dominik Kirst)

Tuesday 16:00-16:30

• Break

Tuesday 16:30-17:45 (Chair: Georges Gonthier)

• Invited Talk: The Lean 4 theorem prover and programming language (Leonardo De Moura)
• Short Talk: Forwarders as Process Compatibility, Logically [slides] (Marco Carbone, Sonia Marin and Carsten Schuermann)

Tuesday 17:45-18:00

• Break

Tuesday 18:00-19:00

• Business Meeting

Tuesday Evening

• “Fête de la musique”: there will be music all around the city, see this listing (in French) for a curated list of events.

Wednesday

Wednesday 9:00-10:25 (Chair: Gert Smolka)

• Invited Talk: Composing Music from Types [slides] (Youyou Cong)
• Long Talk: Strong, Synthetic, and Computational Proofs of Gödel’s First Incompleteness Theorem [slides] (Benjamin Peters and Dominik Kirst)

Wednesday 10:25-10:50

• Break

Wednesday 10:50-12:20 (Chair: Nicolas Tabareau)

• 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 [slides] (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 [slides] (Yannick Forster and Matthieu Sozeau)
• Short Talk: Verification Techniques for Smart Contracts in Agda [slides] (Fahad Alhabardi, Arnold Beckmann, Bogdan Lazar and Anton Setzer)
• Short Talk: Exhaustive testing of property testers (Auke Booij)

Wednesday 12:20-14:00

• Lunch

Wednesday 14:00-14:55 (Chair: Herman Geuvers)

• Long Talk: A Generalized Translation of Pure Type Systems [slides] (Nathan Mull)
• Short Talk: Killing Two Hens with One Stone – Equivalence Between Typed and Untyped Algorithmic Conversions [slides] (Meven Lennon-Bertrand)
• Short Talk: Canonicity and decidability of equality for setoid type theory [slides] (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:25 (Chair: Andreas Abel)

• Invited Talk: Refine and Synthesise: a type-theoretic view on neural network robustness (Ekaterina Komendantskaya)
• Long Talk: The Münchhausen method and combinatory type theory (Thorsten Altenkirch, Ambrus Kaposi, Artjoms Šinkarovs and Tamás Végh)

Thursday 10:25-10:50

• Break

Thursday 10:50-12:30 (Chair: Ambrus Kaposi)

• Long Talk: Resizing Prop down to an axiom [slides] (Stefan Monnier)
• Short Talk: Towards a Formalization of Affine Schemes in Cubical Agda [slides] (Anders Mörtberg and Max Zeuner)
• Short Talk: Higher-Order Universe Operators in Martin-Löf Type Theory with one Mahlo Universe [slides] (Yuta Takahashi)
• Short Talk: A Reasonably Gradual Type Theory [slides] (Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau and Éric Tanter)
• Short Talk: Semantics for two-dimensional type theory [slides] (Benedikt Ahrens, Paige North and Niels van der Weide)
• Short Talk: Synthetic Versions of the Kleene-Post and Post’s Theorem [slides] (Dominik Kirst, Niklas Mück and Yannick Forster)

Thursday 12:30-14:00

• Lunch

Thursday 14:00-15:50 (Chair: Stefan Monnier)

• Long Talk: A Datatype of Planar Graphs [slides] (Malin Altenmüller and Conor McBride)
• Short Talk: Monsters: Programming and Reasoning [slides] (Venanzio Capretta and Christopher Purdy)
• Short Talk: Data Types with Negation [slides] (Robert Atkey)
• Short Talk: Consistent Ultrafinitist Logic [slides] (Michal Gajda)
• Long Talk: Decidability and Semidecidability via ordinals [slides] (Nicolai Kraus, Fredrik Nordvall Forsberg and Chuangjie Xu)
• Short Talk: The Patch Frame of a Spectral Locale in Univalent Type Theory [slides] (Ayberk Tosun and Martín Escardó)

Thursday 15:50-16:00

• Break

Thursday 16:30-17:55 (Chair: Sandra Alves)

• Long Talk: More on modal embeddings and calling paradigms [slides] (José Espírito Santo, Luís Pinto and Tarmo Uustalu)
• Short Talk: Certified Abstract Machines for Skeletal Semantics [slides] (Guillaume Ambal, Sergueï Lenglet and Alan Schmitt)
• Short Talk: Towards a translation from K to Dedukti [slides] (Amélie Ledein, Valentin Blot and Catherine Dubois)
• Short Talk: Validating OCaml soundness by translation into Coq [slides] (Jacques Garrigue and Takafumi Saikawa)
• Short Talk: Small inversions for smaller inversions [slides] (Jean-Francois Monin)

Pre-recorded talks

• Pre-recorded talk: Description Operators in Partial Propositional Type Theory (Víctor Aranda and Manuel Martins) (video)
• Pre-recorded talk: A Domain-Specific Language for Name Modifiers (Kuen-Bang Hou Favonia) (video)
• Pre-recorded talk: Synthetic Tait Computability for Simplicial Type Theory [slides] (Jonathan Weinberger, Benedikt Ahrens, Ulrik Buchholtz and Paige North) (video)
• Pre-recorded talk: Homotopy setoids and quotient completion (Cipriano Cioffo) (video)

This talks can be discussed on the Zulip chat

Accepted Papers

• A Datatype of Planar Graphs [slides] (Malin Altenmüller and Conor McBride)
• A Domain-Specific Language for Name Modifiers (Kuen-Bang Hou Favonia)
• A Flexible Multimodal Proof Assistant [slides] (Philipp Stassen, Daniel Gratzer and Lars Birkedal)
• A Generalized Translation of Pure Type Systems [slides] (Nathan Mull)
• A Reasonably Gradual Type Theory [slides] (Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau and Éric Tanter)
• A Simple Concurrent Lambda Calculus for Encoding Session types [slides] (Jules Jacobs)
• A Theory of Call-by-Value Solvability [slides] (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 [slides] (Yannick Forster and Matthieu Sozeau)
• BioTT: a Family of Brouwerian Intuitionistic Theories Open to Classical Reasoning [slides] (Mark Bickford, Liron Cohen, Robert Constable and Vincent Rahli)
• Canonicity and decidability of equality for setoid type theory [slides] (István Donkó and Ambrus Kaposi)
• Capable GV: Capabilities for Session Types in GV [slides] (Magdalena J. Latifa and Ornela Dardha)
• Certified Abstract Machines for Skeletal Semantics [slides] (Guillaume Ambal, Sergueï Lenglet and Alan Schmitt)
• Conservativity of Two-Level Type Theory Corresponds to Staged Compilation [slides] (András Kovács)
• Consistent Ultrafinitist Logic [slides] (Michal Gajda)
• Cubical models are cofreely parametric [slides] (Hugo Moeneclaey)
• Data Types with Negation [slides] (Robert Atkey)
• Decidability and Semidecidability via ordinals [slides] (Nicolai Kraus, Fredrik Nordvall Forsberg and Chuangjie Xu)
• Deciding the cofibration logic of cartesian cubical type theories [slides] (Robert Rose, Matthew Weaver and Daniel Licata)
• Description Operators in Partial Propositional Type Theory (Víctor Aranda and Manuel Martins)
• Case Study on Displayed Monoidal Categories [slides] (Benedikt Ahrens, Ralph Matthes and Kobe Wullaert)
• Exhaustive testing of property testers (Auke Booij)
• Extending Cubical Agda with Internal Parametricity [slides] (Antoine Van Muylder, Andrea Vezzosi, Andreas Nuyts and Dominique Devriese)
• Extending truth table natural deduction to predicate logic [slides] (Herman Geuvers and Tonny Hurkens)
• Flexible presentations of graded monads [slides] (Shin-Ya Katsumata, Dylan McDermott, Tarmo Uustalu and Nicolas Wu)
• Forwarders as Process Compatibility, Logically [slides] (Marco Carbone, Sonia Marin and Carsten Schuermann)
• From iterated parametricity to indexed semi-cubical and semi-simplicial sets: a formal construction [slides] (Hugo Herbelin and Ramkumar Ramachandra)
• Higher-Order Universe Operators in Martin-Löf Type Theory with one Mahlo Universe [slides] (Yuta Takahashi)
• Homotopy setoids and quotient completion (Cipriano Cioffo)
• Implementing Martin-Löf’s meaning explanations for intuitionistic type theory in Agda [slides] (Peter Dybjer and Anton Setzer)
• Interpreting second-order arithmetic via update recursion [slides] (Valentin Blot)
• Killing Two Hens with One Stone – Equivalence Between Typed and Untyped Algorithmic Conversions [slides] (Meven Lennon-Bertrand)
• Linear lambda-calculus is linear [slides] (Alejandro Díaz-Caro and Gilles Dowek)
• Linear Rank Intersection Types [slides] (Fábio Reis, Sandra Alves and Mário Florido)
• Monsters: Programming and Reasoning [slides] (Venanzio Capretta and Christopher Purdy)
• More on modal embeddings and calling paradigms [slides] (José Espírito Santo, Luís Pinto and Tarmo Uustalu)
• Myhill Isomorphism Theorem and a Computational Cantor-Bernstein Theorem in Constructive Type Theory [slides] (Yannick Forster, Felix Jahn and Gert Smolka)
• Noninvasive Polarized Subtyping for Inductive Types [slides] (Théo Laurent and Kenji Maillard)
• On Dynamic Lifting and Effect Typing in Circuit Description Languages [slides] (Andrea Colledan and Ugo Dal Lago)
• Partial Dijkstra Monads for All [slides] (Théo Winterhalter, Cezar-Constantin Andrici, Catalin Hritcu, Kenji Maillard, Guido Martínez and Exequiel Rivas)
• Pre-bilattices in Univalent Foundations [slides] (Georgios V. Pitsiladis)
• Proof-relevant normalization for intersection types with profunctors [slides] (Zeinab Galal)
• Quantitative Inhabitation in Call-by-Value (Victor Arrial)
• Quantitative Perspectives on Generalized Applications [slides] (Loïc Peyrot)
• Realizing Implicit Computational Complexity [slides] (Clément Aubert, Thomas Rubiano, Neea Rusch and Thomas Seiller)
• Resizing Prop down to an axiom [slides] (Stefan Monnier)
• Semantics for two-dimensional type theory [slides] (Benedikt Ahrens, Paige North and Niels van der Weide)
• Session Type Systems Compared: The Case of Deadlock Freedom [slides] (Ornela Dardha and Jorge A. Pérez)
• Sikkel: Multimode Simple Type Theory as an Agda Library [slides] (Joris Ceulemans, Andreas Nuyts and Dominique Devriese)
• Small inversions for smaller inversions [slides] (Jean-Francois Monin)
• Strong, Synthetic, and Computational Proofs of Gödel’s First Incompleteness Theorem [slides] (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 [slides] (Yannick Forster and Dominik Kirst)
• Synthetic Versions of the Kleene-Post and Post’s Theorem [slides] (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 [slides] (Ayberk Tosun and Martín Escardó)
• Toward a denotational semantics of streams for a verified Lustre compiler [slides] (Paul Jeanmaire, Timothy Bourke and Marc Pouzet)
• Towards a Formalization of Affine Schemes in Cubical Agda [slides] (Anders Mörtberg and Max Zeuner)
• Towards a Mechanized Theory of Computation for Education [slides] (Tiago Cogumbreiro and Yannick Forster)
• Towards a translation from K to Dedukti [slides] (Amélie Ledein, Valentin Blot and Catherine Dubois)
• Towards Higher Observational Type Theory [slides] (Thorsten Altenkirch, Ambrus Kaposi and Mike Shulman)
• Towards Probabilistic Reasoning about Typed Combinatory Terms [slides] (Simona Kašterović and Silvia Ghilezan)
• Transpension: The Right Adjoint to the Pi-Type [slides] (Andreas Nuyts and Dominique Devriese)
• Two Guarded Recursive Powerdomains for Applicative Simulation [slides] (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 [slides] (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 [slides] (Frederik L. Aagaard, Magnus B. Kristensen, Daniel Gratzer and Lars Birkedal)
• Validating OCaml soundness by translation into Coq [slides] (Jacques Garrigue and Takafumi Saikawa)
• Verification Techniques for Smart Contracts in Agda [slides] (Fahad Alhabardi, Arnold Beckmann, Bogdan Lazar and Anton Setzer)