Programme

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)

Comments are closed.

  •  

    Sponsors