Accepted contributions
The following talk proposals have been accepted to TYPES 2026.
- W. Ait-Moussa, Pierre Boutillier, Hugo Herbelin, Meven Lennon-Bertrand, Thierry Martinez, Gabriel Scherer: Compilation of dependent pattern-matching using small inversion [slides]
- Cass Alexandru, Henning Urbat, Thorsten Wißmann: Intrinsically Recursive Coalgebras [slides]
- Jessica Allegro, Martin Baillon, Nuria Brede, Hugo Herbelin, Yannick Forster, Jad Koleilat, Étienne Miquey, Dimitar Mitov: On the logical structure of choice, bar induction, maximality and well-foundedness principles equivalent to the axiom of choice [slides]
- Thorsten Altenkirch, Håkon Robbestad Gylterud, Zhili Tian: Containers in Higher Kinds [slides]
- Thorsten Altenkirch, Christina O'Donnell: Constructing QITs from Quotients [slides]
- Samy Avrillon, Ambrus Kaposi, Ambroise Lafont, Niyousha Najmaei, Johann Rosain: For Generalised Algebraic Theories, Two Sorts are Enough [slides]
- Steve Awodey, Joseph Hua: Path Types in Algebraic Type Theory [slides]
- Reid Barton, Axel Ljungström, Owen Milner, Anders Mörtberg: The Serre finiteness theorem in Cubical Agda [slides]
- Thibaut Benjamin, Camil Champin, Ioannis Markakis: A type theory for invertibility in weak ω-categories [slides]
- Benno van den Berg: Constructive ordinals [slides]
- Marc Bezem, Thierry Coquand, Peter Dybjer, Martin Escardo: A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism [slides]
- Martin Ernst Bidlingmaier: Dependent Datalog [slides]
- Valentin Blot: Sequential algorithms as a Dialectica interpretation [slides]
- John Bourke, Vít Jelínek: Bicolimit Presentations of Type Theories [slides]
- Harry Bryant, Andrew Lawrence, Monika Seisenberger, Anton Setzer: Techniques for Verified Propositional SMT Proof Checking [slides]
- Nathaniel Burke: Smart with [slides]
- Félix Castro, Liron Cohen, Étienne Miquey: Is typed realizability only predicative? [slides]
- Junyuan Chen, Maximilian Doré: Towards a Brown-Palsberg Self-Interpreter for Dependent Types [slides]
- Rahul Chhabra, Carlo Angiuli, Daniel Gratzer: Homomorphisms of structures in simplicial type theory [slides]
- Fernando Chu, Paige Randall North: Dependent-two sided factorization systems for directed type theory [slides]
- Cyril Cohen, Assia Mahboubi, Vojtěch Štěpančík: Generating morphism types using parametricity and Trocq [slides]
- Thierry Coquand, Raphaël Sterbac: Cumulative hierarchies of universes and their equivalence in dependent type theory [slides]
- Stefania Damato, Thorsten Altenkirch: Containers form a Groupoid CwF [slides]
- Nils Anders Danielsson: Towards HoTT with Erased Univalence and Box-Cong [slides]
- Oskar Eriksson: Two-Sided Graded Type Theory, Formalized in Agda [slides]
- Thiago Felicissimo, Yann Leray, Loïc Pujet, Nicolas Tabareau, Éric Tanter, Théo Winterhalter: Definitional Proof Irrelevance Made Accessible [slides]
- Maribel Fernández, Luka Janjić, Nora Szasz, Álvaro Tasistro: Nominal Type Theory [slides]
- Yannick Forster, Dominik Kirst: Constructive Mathematics without any choice [slides]
- Lide Grotenhuis, Daniel Otten: Unravelling Cyclic Proofs into Proofs by Induction [slides]
- Hugo Herbelin, Étienne Miquey: A Computational Interpretation of the Axiom of Choice [slides]
- Joseph Hua, Yiming Xu: Polynomial functors in π-clans and structured semantics of MLTT [slides]
- Timothée Huneau, Yannick Forster, Dominik Kirst, Sam van Gool: Exploring blurred choice axioms for constructive reverse mathematics [slides]
- Tom de Jong, Nicolai Kraus, Axel Ljungström: The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory [slides]
- Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh, Fredrik Nordvall Forsberg: Generalized Decidability via Brouwer Trees [slides]
- Krzysztof Kapulkin, Yufeng Li: Yet another cubical type theory, but via a semantic approach [slides]
- Titouan Leclercq, Étienne Miquey: A robust approach to the computational interpretation of the Fan Theorem [slides]
- Jem Lord: Easy Parametricity [slides]
- Owen Lynch: An Algebraic Approach to the Static/Dynamic Phase Distinction for Module Calculi [slides]
- Julien Marquet-Wagner: Induction-Induction for Intrinsically Well-Scoped Syntaxes [slides]
- Ralph Matthes, Stefan Neuwirth: Dynamical Method via Natural Deduction [slides]
- Owen Milner: Classifying certain group extensions in HoTT [slides]
- Rasmus Ejlers Møgelberg: Multi-clocked Guarded Recursion beyond ω [slides]
- Lorenzo Molena, Marcin Jan Turek-Grzybowski, Riccardo Borsetto: A Cubical Path from Algebra to Analysis [slides]
- Niyousha Najmaei, Niels van der Weide: A General Construction of Strict Models in HoTT [slides]
- Eske Hoy Nielsen, Simon Dima, Lucas Escot, Orestis Melkonian, Hugo Segoufin-Cholet, James Chapman, Yannick Forster, Matthieu Sozeau, Bas Spitters: Peregrine: a middle-end for code generation from proof assistants [slides]
- Jonathan Osser: Sketching type theories in two dimensions [slides]
- Lorenzo Perticone: A Graded Modal Type Theory for Pulse Schedules with Measurements [slides]
- Jeremy Pope: An Intermediate Representation for Quantum Computation [slides]
- Zhuoyuan QU: A Naive Encoding of Russell's Paradox in Type Theory [slides]
- Aarne Ranta, May Ohlsson: Informalization of Advanced Mathematics: A Case Study with Homotopy Type Theory [slides]
- Rob Schellingerhout: Higher Algebra in Simplicial Homotopy Type Theory [slides]
- Tex Schönlank, Andreas Nuyts, Dominique Devriese: Towards FaceTT: a generalization of intensional type systems with Glue [slides]
- Alessandro Sosso, Bas Spitters: Agentic proving for type theory [slides]
- Sam Speight, Niels van der Weide: Impredicative Encodings of Linear Types [slides]
- Sergei Stepanenko, Patrick Bahr, Rasmus Ejlers Møgelberg: A DSL for Guarded Type Theory in Lean [slides]
- Andrew Swan: Counterexamples in Cubical Sets [slides]
- Yuta Takahashi: Towards Functorial Ordinal Notations in Type Theory [slides]
- Yee-Jian Tan, Andreas Nuyts, Dominique Devriese: Towards Computational UIP in Cubical Agda [slides]
- Dominik Wehr, Dominik Kirst: Constructive Reverse Mathematics of Cyclic Proof Theory [slides]
- Szumi Xie: Eliminating Finitary Inductive-Inductive Types Without K [slides]