TYPES 2025: Programme

Talks will take place in room TL325 in the Learning and Teaching Building on the University of Strathclyde campus, with coffee breaks and lunches in the adjacent room TL328 (TL324 on Friday). Invited talks (with yellow background below) are 45 minutes long, and contributed talks are either 15 minutes (light gray background below) or 20 minutes long. The talks that are part of the Women in EPN event on Tuesday afternoon have different timings.

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

Preliminary Programme

Sponsors

Gold sponsor

Bronze sponsors

Other sponsors