TYPES 2025: The 31st International Conference on Types for Proofs and Programs

8:30–09:00 Registration and coffee Coffee Coffee Coffee Coffee 09:00–10:35 Chair: Fredrik Nordvall Forsberg Chair: Robert Atkey Chair: Andreas Abel Chair: Herman Geuvers Chair: Andrew Swan Towards topological type theory for decrypting transfinite methods in classical mathematics [s] [v]
Ingo Blechschmidt Algebraic Universes and Variances For All [s] [v]
Matthieu Sozeau, Marc Bezem Intuitionistic modalities through proof theory [s] [v]
Sonia Marin A Guided Tour of Polarity and Focusing [s] [v]
Chris Martens A constructive higher groupoid model of homotopy type theory [s] [v [v]
Christian Sattler Internalized Parametricity via Lifting Universals [s] [v]
Aaron David Stump Accessible Sets in Martin-Löf Type Theory with Function Extensionality [s] [v]
Yuta Takahashi Extending Sort Polymorphism with Elimination Constraints [s] [v]
Tomás Díaz, Johann Rosain, Matthieu Sozeau, Nicolas Tabareau, Théo Winterhalter Higher-Order Focusing on Linearity and Effects [s] [v]
Siva Somayyajula Compositional memory management in the λ-calculus [s] [v]
Sky Wilshaw, Graham Hutton A Ghost Sort for Proof-Relevant yet Erased Data in Rocq and MetaRocq [s] [v]
Johann Rosain, Matthieu Sozeau, Théo Winterhalter In Cantor Space, No One Can Hear You Stream [s] [v]
Martin Baillon, Assia Mahboubi, Pierre-Marie Pédrot The Case for Impredicative Universe Polymorphism [s] [v]
Stefan Monnier Monadic Equational Reasoning for while loop in Rocq [s] [v]
Ryuji Kawakami, Jacques Garrigue, Takafumi Saikawa, Reynald Affeldt Choice principles and a cotopological modality in HoTT [s] [v]
Owen Milner A Fully Dependent Assembly Language [s] [v]
Yulong Huang, Jeremy Yallop Examples and counter-examples of injective types in univalent mathematics [s] [v]
Tom de Jong, Martin Escardo From parametricity to identity types [s] [v]
Thorsten Altenkirch, Ambrus Kaposi, Michael Shulman, Elif Üsküplü Commuting Rules for the Later Modality and Quantifiers in Step-Indexed Logics [s] [v]
Bálint Kocsis, Robbert Krebbers Towards Modular Composition of Inductive Types Using Lean Meta-programming [s] [v]
Ramy Shahin Efficient Program Extraction in Elementary Number Theory using the Proof Assistant Minlog [s] [v]
Franziskus Wiesnet 10:35–11:00 Coffee break Coffee break Coffee break Coffee break Coffee break 11:00–12:30 Chair: Guillaume Allais Chair: Tom de Jong Chair: András Kovács Chair: Liang-Ting Chen Chair: Kenji Maillard A Coq Formalization of Lagois Connections for Secure Information Flow [s] [v]
Casper Ståhl, Léon Gondelman, René Rydhof Hansen, Danny Bøgsted Poulsen About the construction of simplicial and cubical sets in indexed form: the case of degeneracies [s] [v]
Hugo Herbelin, Ramkumar Ramachandra How (not) to prove typed type conversion transitive [s] [v]
Yann Leray Type-safe Bidirectional Channels in Idris 2 [s] [v]
Guillaume Allais Linear Types inside Dependent Type Theory [s] [v]
Maximilian Doré Coq proof of the fifth Busy Beaver value [s] [v]
Tristan Stérin, the bbchallenge Collaboration Predicative Stone Duality in Univalent Foundations [s] [v]
Ayberk Tosun, Martin Escardo Arrow algebras [s] [v]
Benno van den Berg, Marcus Briët, Umberto Tarantino Code Generation via Meta-programming in Dependently Typed Proof Assistants [s] [v]
Mathis Bouverot-Dupuis, Yannick Forster Impredicative Encodings of Inductive and Coinductive Types [s] [v]
Herman Geuvers, Niels van der Weide, Steven Bronsveld Mechanizing logical relations [s] [v]
Josselin Poiret Cocompleteness in simplicial homotopy type theory [s] [v]
Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz Weak Equality Reflection in MLTT with Propositional Truncation [s] [v]
Felix Bradley, Zhaohui Luo Towards Being Positively Negative about Dependent Types [s] [v]
Jan de Muijnck-Hughes NbE for LNL via Adjoint Meta-modalities [s] [v]
James Wood Geometric Reasoning in Lean: from Algebraic Structures to Presheaves [s] [v]
Kenji Maillard, Yiming Xu Yet another homotopy group, yet another Brunerie number [s] [v]
Tom Jack, Axel Ljungström Towards Quotient Inductive Types in Observational Type Theory [s] [v]
Thiago Felicissimo, Nicolas Tabareau Implementing a Typechecker for an Esoteric Language: Experiences, Challenges, and Lessons [s] [v]
Alex Rice Unboxed Dependent Types [s] [v]
Constantine Theocharis, Ellis Kesterton Löb's Theorem and Provability Predicates in Rocq [s] [v]
Janis Bailitis, Dominik Kirst, Yannick Forster Rezk completions For (Elementary) Topoi [s] [v]
Kobe Wullaert, Niels van der Weide Matching (Co)patterns with Cyclic Proofs [s] [v]
Lide Grotenhuis, Daniël Otten A Two-level Foundation for the Calculus of Constructions [s] [v]
Pietro Sabelli, Maria Emilia Maietti A Quantitative Dependent Type Theory with Recursion [s] [v]
Oskar Eriksson, Nils Anders Danielsson, Andreas Abel 12:30–13:30 Lunch break Lunch break Lunch & Coffee break Lunch & Coffee break Lunch & Coffee break 13:30–14:10 Chair: Théo Winterhalter Chair: Benno van den Berg Chair: Malin Altenmüller Chair: Ambrus Kaposi Chair: Håkon Gylterud Expansion in a Calculus with Explicit Substitutions [s] [v]
Ana Jorge Almeida, Sandra Alves, Mário Florido Type Theory and Philosophical Logic [s] [v]
Greg Restall Towards a computational quantum logic [s] [v]
Alejandro Díaz-Caro A Timed Predicate Temporal Logic Sequent Calculus [s] [v]
Javier Enriquez Mendoza, Sam Speight, Vincent Rahli Stellar — A Library for API Programming [s] [v]
André Videla Presheaves on Purpose [s] [v]
Conor Mc Bride Constructive algebraic completeness of first-order bi-intuitionistic logic [s] [v]
Dominik Kirst, Ian Shillito Internal Proofs of Strong Normalization [s] [v]
Cody Roux Verfying Z3 RUP Proofs with the Interactive Theorem Provers Coq/Rocq and Agda [s] [v]
Harry Bryant, Andrew Lawrence, Monika Seisenberger, Anton Setzer An Inductive Universe for Setoids [s] [v]
Loïc Pujet 14:10–15:00 Thinning Thinnings: Safe and Efficient Binders [s] [v]
April Gonçalves, Wen Kokke Chair: Sandra Alves Excursion to Loch Lomond
Formalising Monitors for Distributed Deadlock Detection [s] [v]
Radosław Jan Rowicki, Adrian Francalanza, Alceste Scalas Weihrauch Problems as Containers [s] [v]
Ian Price, Cécilia Pradic WEPN Opening and Welcome
Ecumenical logic [s] [v]
Elaine Pimentel (14:15–15:15) Categorical Normalization by Evaluation: A Novel Universal Property for Syntax [s] [v]
David G. Berry, Marcelo Fiore Fair Termination for Resource-Aware Active Objects [s] [v]
Francesco Dagnino, Paola Giannini, Violet Ka I Pun, Ulises Torrella Containers: Compositionality for Tensors [s] [v]
Neil Ghani, Pierre Hyvernat, Artjoms Sinkarovs Rational Codata as Syntax-with-Binding: Correct-by-Construction Foundations of the Modal μ-Calculus [s] [v]
Sean Watters Mechanized safety of Jolteon consensus in Agda [s] [v]
Orestis Melkonian, Mauro Jaskelioff, James Chapman Large Elimination and Indexed Types in Refinement Types [s] [v]
Alessio Ferrarini, Niki Vazou 15:00–15:30 Coffee break Coffee break (15:15–15:45) Coffee break Coffee break 15:30–17:00 Chair: Thorsten Altenkirch Chair: Sandra Alves Chair: Dominik Kirst Chair: Niels van der Weide Dependent two-sided fibrations for directed type theory [s] [v]
Fernando Chu, Paige Randall North Reasoning with strict symmetric monoidal categories in Agda [s] [v]
Malin Altenmüller (15:45–16:15) Canonical Bidirectional Typing via Polarised System L [s] [v]
Zanzi Mihejevs HoTTLean: Formalizing the Meta-Theory of HoTT in Lean [s] [v]
Joseph Hua, Steve Awodey, Mario Carneiro, Sina Hazratpour, Wojciech Nawrocki, Spencer Woolfson, Yiming Xu Synthetic-Inductive Category Theory [s] [v]
Jacob Neumann An existential-free theory of arithmetic in all finite types [s] [v]
Makoto Fujiwara Representing type theories in two-level type theory [s] [v]
Nicolai Kraus, Tom de Jong Directed equality with dinaturality [s] [v]
Andrea Laretto, Fosco Loregian, Niccolò Veltri Type Theory of Acyclic and Cyclic Algorithms without Chain Memory [s] [v]
Roussanka Loukanova (16:15–16:45) A Generalized Logical Framework [s] [v]
András Kovács, Christian Sattler Lean4Lean: Mechanizing the Metatheory of Lean [s] [v]
Mario Carneiro A Type Theory for Comprehension Categories with Applications to Subtyping [s] [v]
Niyousha Najmaei, Niels van der Weide, Benedikt Ahrens, Paige Randall North A Curry-Howard correspondence for intuitionistic inquisitive logic [s] [v]
Ivo Pezlar, Vít Punčochář Solving Guarded Domain Equations in Presheaves Over Ordinals and Mechanizing It [s] [v]
Sergei Stepanenko, Amin Timany 15 minute break 15 minute break
(16:45–17:00) Y is not typable in λ U [s] [v]
Herman Geuvers, Joep Verkoelen 15 minute break 17:00–18:15 Chair: Nicolai Kraus Discussion on gender balance issues [s]
(17:00–18:30) TYPES Business Meeting [s]
Chair: Rasmus Møgelberg Irregular models of type theory [s] [v]
Andrew Wakelin Swan Cohomology in Synthetic Stone Duality [s] [v]
Hugo Moeneclaey, Thierry Coquand, Felix Cherubini, Freek Geerligs An algebraic internal groupoidal model of Martin-Löf type theory [s] [v]
Calum Hughes Towards Formalising the Guard Checker of Rocq [s] [v]
Yee-Jian Tan, Yannick Forster Realizability Triposes from Sheaves [s] [v]
Bruno da Rocha Paiva, Vincent Rahli Extensional concepts in intensional type theory, revisited [s]
Yufeng Li, Krzysztof Kapulkin AdapTT: A Type Theory with Functorial Types [s] [v]
Arthur Adjedj, Thibaut Benjamin, Meven Lennon-Bertrand, Kenji Maillard Lightweight Agda Formalization of Denotational Semantics [s] [v]
Peter D. Mosses 18:15–19:30 Welcome Reception
Level 11, Livingstone Tower 19:30–22:00 Conference Dinner
Grosvenor Cafe