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)