Accepted contributions

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

Sponsors

Gold sponsor

Bronze sponsors

Other sponsors