Accepted contributions

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

Sponsors

Gold sponsor

Bronze sponsors

Other sponsors