Volume
LIPIcs, Volume 384
31st International Conference on Types for Proofs and Programs (TYPES 2025)
Event
Editors
Publication Details
- published at: 2026-07-30
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-441-3
Access Numbers
- Detailed Access Statistics available here
-
Total Accesses (updated on a weekly basis)
0Documents
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 384, TYPES 2025, Complete Volume
Abstract
LIPIcs, Volume 384, TYPES 2025, Complete Volume
Cite as
31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 1-346, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Proceedings{nordvallforsberg_et_al:LIPIcs.TYPES.2025,
title = {{LIPIcs, Volume 384, TYPES 2025, Complete Volume}},
booktitle = {31st International Conference on Types for Proofs and Programs (TYPES 2025)},
pages = {1--346},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-441-3},
ISSN = {1868-8969},
year = {2026},
volume = {384},
editor = {Nordvall Forsberg, Fredrik and McKinna, James},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025},
URN = {urn:nbn:de:0030-drops-275021},
doi = {10.4230/LIPIcs.TYPES.2025},
annote = {Keywords: LIPIcs, Volume 384, TYPES 2025, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{nordvallforsberg_et_al:LIPIcs.TYPES.2025.0,
author = {Nordvall Forsberg, Fredrik and McKinna, James},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {31st International Conference on Types for Proofs and Programs (TYPES 2025)},
pages = {0:i--0:x},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-441-3},
ISSN = {1868-8969},
year = {2026},
volume = {384},
editor = {Nordvall Forsberg, Fredrik and McKinna, James},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.0},
URN = {urn:nbn:de:0030-drops-275014},
doi = {10.4230/LIPIcs.TYPES.2025.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Choice Principles and Hypercompletion in HoTT
Abstract
Building on work of Anel and Barton [M. Anel and R. Barton, 2024], we will introduce the construction of a hypercompletion modality [E. Rijke et al., 2020] in HoTT under the assumption that countable choice holds. Central results have been formalized in Cubical Agda and will be referenced where appropriate.
Cite as
Owen Milner. Choice Principles and Hypercompletion in HoTT. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 1:1-1:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{milner:LIPIcs.TYPES.2025.1,
author = {Milner, Owen},
title = {{Choice Principles and Hypercompletion in HoTT}},
booktitle = {31st International Conference on Types for Proofs and Programs (TYPES 2025)},
pages = {1:1--1:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-441-3},
ISSN = {1868-8969},
year = {2026},
volume = {384},
editor = {Nordvall Forsberg, Fredrik and McKinna, James},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.1},
URN = {urn:nbn:de:0030-drops-270193},
doi = {10.4230/LIPIcs.TYPES.2025.1},
annote = {Keywords: HoTT, hypercompletion, modalities}
}
Document
Lean4Lean: Verifying a Typechecker for Lean, in Lean
Abstract
In this paper we present a new "external checker" for the Lean theorem prover, written in Lean itself. This is the first complete typechecker for Lean 4 other than the reference implementation in C++ used by Lean itself, and our new checker is competitive with the original, running between 20% and 50% slower and usable to verify all of Lean’s Mathlib library, taking an additional step in Lean’s aim to self-host the full elaborator and compiler. Moreover, because the checker is written in a language which admits formal verification, it is possible to state and prove properties about the kernel itself, and we report on progress to formalize the Lean type theory abstractly and prove some theorems about it. Finally, we combine these to get a proof of correctness of parts of the kernel. We plan to use this project to help justify any future changes to the kernel and type theory and ensure unsoundness does not sneak in through either the abstract theory or implementation bugs. The verification is already paying off, as one soundness bug has been spotted and fixed as a result of this work.
Cite as
Mario Carneiro. Lean4Lean: Verifying a Typechecker for Lean, in Lean. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 2:1-2:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{carneiro:LIPIcs.TYPES.2025.2,
author = {Carneiro, Mario},
title = {{Lean4Lean: Verifying a Typechecker for Lean, in Lean}},
booktitle = {31st International Conference on Types for Proofs and Programs (TYPES 2025)},
pages = {2:1--2:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-441-3},
ISSN = {1868-8969},
year = {2026},
volume = {384},
editor = {Nordvall Forsberg, Fredrik and McKinna, James},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.2},
URN = {urn:nbn:de:0030-drops-270206},
doi = {10.4230/LIPIcs.TYPES.2025.2},
annote = {Keywords: Lean, proof assistant, external typechecker, implementation, metatheory, type theory, proof theory}
}
Document
Symmetries in Sorting
Abstract
Sorting algorithms are fundamental to computer science, and their correctness criteria are well understood as rearranging elements of a list according to a specified total order on the underlying set of elements. As mathematical functions, they are functions on lists that perform combinatorial operations on the representation of the input list. In this paper, we study sorting algorithms conceptually as abstract sorting functions.
There is a canonical surjection from the free monoid on a set (lists of elements) to the free commutative monoid on the same set (multisets of elements). We show that sorting functions determine a section (right inverse) to this surjection satisfying two axioms, that do not presuppose a total order on the underlying set. Then, we establish an equivalence between (decidable) total orders on the underlying set and correct sorting functions.
The first part of the paper develops concepts from universal algebra from the point of view of functorial signatures, and gives constructions of free monoids and free commutative monoids in (univalent) type theory. Using these constructions, the second part of the paper develops the axiomatisation of sorting functions. The paper uses informal mathematical language, and comes with an accompanying formalisation in Cubical Agda.
Cite as
Vikraman Choudhury and Wind Wong. Symmetries in Sorting. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 3:1-3:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{choudhury_et_al:LIPIcs.TYPES.2025.3,
author = {Choudhury, Vikraman and Wong, Wind},
title = {{Symmetries in Sorting}},
booktitle = {31st International Conference on Types for Proofs and Programs (TYPES 2025)},
pages = {3:1--3:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-441-3},
ISSN = {1868-8969},
year = {2026},
volume = {384},
editor = {Nordvall Forsberg, Fredrik and McKinna, James},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.3},
URN = {urn:nbn:de:0030-drops-270210},
doi = {10.4230/LIPIcs.TYPES.2025.3},
annote = {Keywords: universal algebra, type theory, homotopy type theory, cubical Agda, constructive mathematics, univalent mathematics, sorting, combinatorics, formalisation}
}
Document
HoTT Operads
Abstract
Internalising classes of datatypes has been a longstanding pursuit in type theory. For example, containers capture strictly positive types, while combinatorial species capture finitely labelled structures. To date, however, there has been no similar attempt to internalise classes of operations on datatypes. In this paper we show how the theory of operads, which extend species with a well-behaved notion of composition, provides a natural approach to internalising finitary operations. We present an internalisation of a generalised notion of operad in homotopy type theory, which provides a generic framework for capturing and reasoning about operations with particular algebraic properties. All our results are formalised in Cubical Agda.
Cite as
Brandon Hewer and Graham Hutton. HoTT Operads. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 4:1-4:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{hewer_et_al:LIPIcs.TYPES.2025.4,
author = {Hewer, Brandon and Hutton, Graham},
title = {{HoTT Operads}},
booktitle = {31st International Conference on Types for Proofs and Programs (TYPES 2025)},
pages = {4:1--4:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-441-3},
ISSN = {1868-8969},
year = {2026},
volume = {384},
editor = {Nordvall Forsberg, Fredrik and McKinna, James},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.4},
URN = {urn:nbn:de:0030-drops-270228},
doi = {10.4230/LIPIcs.TYPES.2025.4},
annote = {Keywords: operads, homotopy type theory, proof assistants}
}
Document
A Graded Modal Type Theory for Pulse Schedules
Abstract
The operations to be performed by a quantum computer are almost invariably given in the form of a quantum circuit. In the final stage of compilation, a quantum circuit must be translated into the input signals accepted by the quantum hardware itself. For a quantum computer based on superconducting qubits, this will be a sequence of microwave control pulses to be sent to the various input channels. A pulse schedule gives a full specification for which pulse should be applied to which channel at what time. There is as yet no language for these pulse schedules that is very amenable to formal semantics.
In this paper, we propose such a language called GRAMPUS (GRAded Modal type theory for PUlse Schedules). It is a graded modal type theory, where the grades represent timing information: a variable x :^{50} Q₁ will represent a state of qubit Q₁ that will exist 50 nanoseconds in the future, and a variable y :^{-75} Q₂ will represent a state of qubit Q₂ that existed 75 nanoseconds in the past.
We give the syntax for two type theories, one with grades (the annotated language) and one without (the plain language). We prove some metatheoretic properties, and describe the semantics in terms of category theory. We show that the input signals to a quantum chip forms a model of the annotated language. We also give a syntactic model, prove that it is initial, and hence prove soundness and completeness theorems.
Cite as
Robin Adams, Jean-Philippe Bernardy, Lorenzo Perticone, and Jeremy Pope. A Graded Modal Type Theory for Pulse Schedules. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 5:1-5:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{adams_et_al:LIPIcs.TYPES.2025.5,
author = {Adams, Robin and Bernardy, Jean-Philippe and Perticone, Lorenzo and Pope, Jeremy},
title = {{A Graded Modal Type Theory for Pulse Schedules}},
booktitle = {31st International Conference on Types for Proofs and Programs (TYPES 2025)},
pages = {5:1--5:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-441-3},
ISSN = {1868-8969},
year = {2026},
volume = {384},
editor = {Nordvall Forsberg, Fredrik and McKinna, James},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.5},
URN = {urn:nbn:de:0030-drops-270237},
doi = {10.4230/LIPIcs.TYPES.2025.5},
annote = {Keywords: Quantum computing, superconducting qubits, linear type theory, graded modal type theory}
}
Document
Formalisation and Extension of Lagois Connections for Secure Information Flow
Abstract
Lagois connections have been proposed as a way to formulate and formalise a secure information flow policy between two organisations each with their own information flow policies that must also be enforced. By composing Lagois connections in a chain, it is possible to compose the information flow policies of several organisations. However, chains are not always suitable. For example, if one of the "links" in the chain enforces a coarser policy than the surrounding links, this corresponds to taking low security information as input and reclassifying it as high security, preventing further communication of (formerly low) information at the low security level. This is an instance of the well-known problem of "label creep".
In this paper we extend the compositionality results of Lagois connections to forests, and graphs that "behave" like forests, of Lagois connections. In addition to the extra flexibility gained in the communication topology, it also solves the label creep problem: Intuitively, to bypass the problematic intermediary, we can verify that the subgraph bypassing the problematic intermediary is located in a forest of secure sub-graphs. We show that this is sound with respect to noninterference, by proving that if information in a program flows according to a secure graph then an attacker can never observe a policy violation in the system.
As a further contribution of this paper, all of the above has been formalised in the Rocq proof assistant, including a novel formalisation of a substantial part of the literature of Lagois connections, providing a strong foundation for future work and implementations.
Cite as
Casper Ståhl, Levs Gondelman, René Rydhof Hansen, and Danny Bøgsted Poulsen. Formalisation and Extension of Lagois Connections for Secure Information Flow. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 6:1-6:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{stahl_et_al:LIPIcs.TYPES.2025.6,
author = {St\r{a}hl, Casper and Gondelman, Levs and Hansen, Ren\'{e} Rydhof and Poulsen, Danny B{\o}gsted},
title = {{Formalisation and Extension of Lagois Connections for Secure Information Flow}},
booktitle = {31st International Conference on Types for Proofs and Programs (TYPES 2025)},
pages = {6:1--6:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-441-3},
ISSN = {1868-8969},
year = {2026},
volume = {384},
editor = {Nordvall Forsberg, Fredrik and McKinna, James},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.6},
URN = {urn:nbn:de:0030-drops-270247},
doi = {10.4230/LIPIcs.TYPES.2025.6},
annote = {Keywords: Lagois connection, information flow, security}
}
Document
Towards Fuzzy Constructive Type Theories
Abstract
In this paper, we explore combinations of Fuzzy Logic and Constructive Higher Order Type Theory. Although Fuzzy Logic is more than 60 years old, and Fuzzy Type Theories have been studied in the classical case of Church’s Theory of Types, there is yet no satisfactory understanding of how to deal with judgements of the shape Γ⊢ M:_d A, where d is a fuzzy degree of confidence. Addressing this issue is important in view of the growing interest in quantitative and non-idempotent type theories. To this end, we introduce fuzzy type assignment systems in order to investigate how minimal fuzzy formulæbehave as types, according to some fuzzy proposition-as-types paradigm. Moreover, we study a fuzzy version of intersection types. In both systems assumptions are multisets and d, in Γ⊢ M:_d A, is a formula of minimal propositional Fuzzy Logic. Evaluating d in a residuated lattice [0,1], endowed with a left-continuous T-norm, we can analyse how the degree of confidence propagates from the assumptions to the conclusion, thereby yielding new information on the derivation. The former system sheds light on the connection between minimal Fuzzy Logics and affine λ-calculus and permits to show that the tautologies in the BCK-logic amount to the simple types which are inhabited by BCK-combinators. The latter system keeps track of the number of times a given fuzzy assumption is made. We discuss the standard suite of metatheorems (inversion lemmata and subject-conversion) for the systems, and point to possible uses of the fuzzy formula attached to the membership construct.
Cite as
Besik Dundua, Furio Honsell, Temur Kutsia, Marina Lenisa, and Luigi Liquori. Towards Fuzzy Constructive Type Theories. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{dundua_et_al:LIPIcs.TYPES.2025.7,
author = {Dundua, Besik and Honsell, Furio and Kutsia, Temur and Lenisa, Marina and Liquori, Luigi},
title = {{Towards Fuzzy Constructive Type Theories}},
booktitle = {31st International Conference on Types for Proofs and Programs (TYPES 2025)},
pages = {7:1--7:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-441-3},
ISSN = {1868-8969},
year = {2026},
volume = {384},
editor = {Nordvall Forsberg, Fredrik and McKinna, James},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.7},
URN = {urn:nbn:de:0030-drops-270256},
doi = {10.4230/LIPIcs.TYPES.2025.7},
annote = {Keywords: Fuzzy type theory, constructive type theory, lambda calculus, residuated lattices}
}
Document
The Rezk Completion for Elementary Topoi
Abstract
The development of category theory in univalent foundations and the formalization thereof is an active field of research. Categories in that setting are often assumed to be univalent which means that identities and isomorphisms of objects coincide. One consequence hereof is that equivalences and identities coincide for univalent categories and that structure on univalent categories transfers along equivalences. However, constructions such as the Kleisli category, the Karoubi envelope, and the tripos-to-topos construction, do not necessarily give univalent categories. To deal with that problem, one uses the Rezk completion, which completes a category into a univalent one. However, to use the Rezk completion when considering categories with structure, one also needs to show that the Rezk completion inherits the structure from the original category.
In this work, we present a modular framework for lifting the Rezk completion from categories to categories with structure. We demonstrate the modularity of our framework by lifting the Rezk completion from categories to elementary topoi in manageable steps.
Cite as
Kobe Wullaert and Niels van der Weide. The Rezk Completion for Elementary Topoi. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 8:1-8:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{wullaert_et_al:LIPIcs.TYPES.2025.8,
author = {Wullaert, Kobe and van der Weide, Niels},
title = {{The Rezk Completion for Elementary Topoi}},
booktitle = {31st International Conference on Types for Proofs and Programs (TYPES 2025)},
pages = {8:1--8:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-441-3},
ISSN = {1868-8969},
year = {2026},
volume = {384},
editor = {Nordvall Forsberg, Fredrik and McKinna, James},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.8},
URN = {urn:nbn:de:0030-drops-270260},
doi = {10.4230/LIPIcs.TYPES.2025.8},
annote = {Keywords: univalent foundations, univalent categories, Rezk completions, UniMath, formalization, elementary topoi}
}
Document
Kleisli Categories with Display Maps
Abstract
In this paper, we show that the Kleisli category C_T for a monad T : C → C is sometimes a structured display map category, meaning that it provides a minimal categorical setting for dependent type theory. If the underlying category C is itself a (structured) display map category, we prove that under mild conditions the canonical functor F_T : C → C_T induces a bijection between the contexts, types, and terms of both C and C_T, thus establishing a kind of "collapsing" result. Finally, we provide several examples and nonexamples, most notably showing that Δ^op equipped with the class of surjective maps is a (structured) display map category.
Cite as
Moana Jubert. Kleisli Categories with Display Maps. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{jubert:LIPIcs.TYPES.2025.9,
author = {Jubert, Moana},
title = {{Kleisli Categories with Display Maps}},
booktitle = {31st International Conference on Types for Proofs and Programs (TYPES 2025)},
pages = {9:1--9:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-441-3},
ISSN = {1868-8969},
year = {2026},
volume = {384},
editor = {Nordvall Forsberg, Fredrik and McKinna, James},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.9},
URN = {urn:nbn:de:0030-drops-270276},
doi = {10.4230/LIPIcs.TYPES.2025.9},
annote = {Keywords: Kleisli categories, Structured display map categories, Dependent type theory}
}
Document
Type-Theoretic Replacement and Univalent Completion: Applications and Interpretations
Abstract
We study Rijke’s type theoretic axiom of replacement, which closes a type-theoretic universe under certain images, and its cousin the axiom of univalent completions, which postulates an extension of each type family to a univalent family. In a long expository section, we survey applications of these two axioms in the literature, from the construction of truncations to the construction of Eilenberg-MacLane spaces to the interpretation of material set theory, making a case for their value as foundational principles. We then give direct, constructive interpretations of the axioms in cubical sets models of type theory and suggest how they can be understood as higher inductive constructions.
Cite as
Evan Cavallo and Thierry Coquand. Type-Theoretic Replacement and Univalent Completion: Applications and Interpretations. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 10:1-10:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{cavallo_et_al:LIPIcs.TYPES.2025.10,
author = {Cavallo, Evan and Coquand, Thierry},
title = {{Type-Theoretic Replacement and Univalent Completion: Applications and Interpretations}},
booktitle = {31st International Conference on Types for Proofs and Programs (TYPES 2025)},
pages = {10:1--10:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-441-3},
ISSN = {1868-8969},
year = {2026},
volume = {384},
editor = {Nordvall Forsberg, Fredrik and McKinna, James},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.10},
URN = {urn:nbn:de:0030-drops-270286},
doi = {10.4230/LIPIcs.TYPES.2025.10},
annote = {Keywords: Homotopy type theory, axiom of replacement, univalent completion, higher inductive type, cubical sets}
}
Document
Multi-Clocked Guarded Recursion Beyond ω
Abstract
Type theories with multi-clocked guarded recursion provide a flexible framework for programming with coinductive types encoding productivity in types. Combining this with solutions to general guarded domain equations one can also construct relatively simple denotational models of programming languages with advanced features. These constructions have previously been explored in the setting of extensional type theory through a presheaf model, which proves correctness of encodings of W-types. That model has been adapted to presheaves of cubical sets (functors into the category of cubical sets), where the model verifies correctness of encodings also of coinductive types whose definitions involve quotient inductive types such as finite powersets or finite distributions. Likewise the cubical model also verifies correctness of coinductive predicates defined using existential quantification and allows the results to be related to the global world of cubical sets.
This paper looks at how to extend the extensional presheaf model of multi-clocked guarded recursion to higher ordinals, so that correctness of encodings of coinductive types can be extended from W-types to those involving finite powersets and finite distributions, as well as coinductive predicates involving existential quantification. This extension will allow results previously proved in Clocked Cubical Type Theory to be interpreted in a model based on set-theory, proving the correctness of these results as understood in their usual set theoretic interpretation.
Cite as
Rasmus Ejlers Møgelberg. Multi-Clocked Guarded Recursion Beyond ω. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 11:1-11:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{mogelberg:LIPIcs.TYPES.2025.11,
author = {M{\o}gelberg, Rasmus Ejlers},
title = {{Multi-Clocked Guarded Recursion Beyond \omega}},
booktitle = {31st International Conference on Types for Proofs and Programs (TYPES 2025)},
pages = {11:1--11:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-441-3},
ISSN = {1868-8969},
year = {2026},
volume = {384},
editor = {Nordvall Forsberg, Fredrik and McKinna, James},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.11},
URN = {urn:nbn:de:0030-drops-270297},
doi = {10.4230/LIPIcs.TYPES.2025.11},
annote = {Keywords: Guarded Recursion, Coinductive Types, Dependent Type Theory, Accessible Functors, Algebraic Theories}
}
Document
Nominal Type Theory by Nullary Internal Parametricity
Abstract
There are many ways to represent the syntax of a language with binders. In particular, nominal frameworks are metalanguages that feature (among others) name abstraction types, which can be used to specify the type of binders. The resulting syntax representation, nominal data types, makes alpha-equivalent terms equal, has a closed induction principle and is well-behaved w.r.t. weakening. It is known that name abstraction types can be presented either as an existential or as a universal quantification on names. Existential name abstractions support matching on name-binding patterns but have cumbersome typing rules; universal ones have clean rules but apparently no such nominal matching. In this work we show that this matching ability and other nominal features are recovered in a type theory consisting of (1) Nullary (0-ary) Internally Parametric Type Theory (nullary PTT), (2) a type of names and a novel name induction principle, (3) nominal data types. This type theory is a legitimate nominal framework: it has universal and (non-primitive) existential name abstractions, a freshness type former, restricted name swapping and local-scope operations. Nominal pattern matching is recovered via term-relevant nullary parametricity. We provide an example involving synthetic Kripke parametricity.
Cite as
Antoine Van Muylder, Andreas Nuyts, and Dominique Devriese. Nominal Type Theory by Nullary Internal Parametricity. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{vanmuylder_et_al:LIPIcs.TYPES.2025.12,
author = {Van Muylder, Antoine and Nuyts, Andreas and Devriese, Dominique},
title = {{Nominal Type Theory by Nullary Internal Parametricity}},
booktitle = {31st International Conference on Types for Proofs and Programs (TYPES 2025)},
pages = {12:1--12:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-441-3},
ISSN = {1868-8969},
year = {2026},
volume = {384},
editor = {Nordvall Forsberg, Fredrik and McKinna, James},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.12},
URN = {urn:nbn:de:0030-drops-270300},
doi = {10.4230/LIPIcs.TYPES.2025.12},
annote = {Keywords: Nominal techniques, Parametricity}
}
Document
A Data Type of Intrinsically Plane Graphs in Agda
Abstract
This work develops a suitable data type for plane graph embeddings in Agda. Graphs are used as combinatorial representations for string diagrams, a graphical calculus for monoidal categories. Whenever a monoidal theory does not include any symmetry or braiding operations, it describes processes that are sensitive to their topology. To encode this information in the graphical language, we have to consider surface-embeddings of graphs. We study the simplest case, plane graphs, and present their implementation in Agda. We overcome issues like the cyclic nature of a graph by using one of its spanning trees as an underlying inductive structure. The graphs we implement are plane by construction and any operation on them is guaranteed to preserve this planarity. Additionally, we present a notion of focussing on a certain subgraph within a graph. This operation is crucial for the application of local rewrite rules which themselves are at the centre of diagrammatic reasoning in monoidal categories.
Cite as
Malin Altenmüller and Conor Titania Mc Bride. A Data Type of Intrinsically Plane Graphs in Agda. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 13:1-13:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{altenmuller_et_al:LIPIcs.TYPES.2025.13,
author = {Altenm\"{u}ller, Malin and Mc Bride, Conor Titania},
title = {{A Data Type of Intrinsically Plane Graphs in Agda}},
booktitle = {31st International Conference on Types for Proofs and Programs (TYPES 2025)},
pages = {13:1--13:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-441-3},
ISSN = {1868-8969},
year = {2026},
volume = {384},
editor = {Nordvall Forsberg, Fredrik and McKinna, James},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.13},
URN = {urn:nbn:de:0030-drops-270312},
doi = {10.4230/LIPIcs.TYPES.2025.13},
annote = {Keywords: planar graph, spanning tree, dependent types, graph rewriting}
}
Document
Functional Representability in Local Set Theories
Abstract
In general local set theories (LST), there is an incomplete representability as (x↦τ) for syntactic functions, i.e. those given by descriptions of the form ∀ x∃!yγ, for some formula γ. The well-known equivalence theorem establishes among other things that it is possible to produce a well-termed local set theory that extends any given LST. However, the natural translation between the corresponding languages still does not guarantee strict functional representability, but only up to isomorphisms.
In this report, natural isomorphisms that are compatible with reasoning internally in the original LST are made explicit and explored in more generality. The internal translation along them is exhibited to be compatible with all logical operations; syntactic functions naturally represent themselves in a robust way as described in the main results.
Cite as
Enrique Ruiz Hernández and Pedro Solórzano. Functional Representability in Local Set Theories. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 14:1-14:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{ruizhernandez_et_al:LIPIcs.TYPES.2025.14,
author = {Ruiz Hern\'{a}ndez, Enrique and Sol\'{o}rzano, Pedro},
title = {{Functional Representability in Local Set Theories}},
booktitle = {31st International Conference on Types for Proofs and Programs (TYPES 2025)},
pages = {14:1--14:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-441-3},
ISSN = {1868-8969},
year = {2026},
volume = {384},
editor = {Nordvall Forsberg, Fredrik and McKinna, James},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.14},
URN = {urn:nbn:de:0030-drops-270323},
doi = {10.4230/LIPIcs.TYPES.2025.14},
annote = {Keywords: local set theories, function symbols, categorical logic}
}
Document
Mendler Dialgebras and Recursion Schemes of Mixed Variance
Abstract
We introduce the notion of Mendler dialgebra and provide a categorical semantics of recursion schemes of mixed variance in its terms. The Mendler-style approach - which employs second-order inference rules - to recursion schemes of mixed variance was championed by Uustalu and Vene in [Uustalu and Vene, 1999] using dinatural transformations, and we generalize their methods to include a variety of new recursion schemes including those presented by Ahn-Sheard in [Ahn and Sheard, 2011], and Stump et al. in [Aaron Stump et al., 2020]. We give sufficient criteria for reducibility of Mendler dialgebras to Lambek algebras [Joachim Lambek, 1968] which correspond to first-order inference rules. A similar reduction in elementary terms for the special case of the systems studied in [Uustalu and Vene, 1999] had been given by the authors, but our approach differs in that we use the language of two-sided fibrations [Street, 1974] to express the reduction for our generalization. This reveals that the "diagonal" of every two-sided fibration with a fibered initial object is isomorphic to a category of Lambek algebras; a dual version concerning reduction to Lambek coalgebras, as well as to bialgebras (inserters), [Joachim Lambek, 1970] is given. We also discuss various properties and examples of Mendler dialgebras, including higher-order abstract syntax which is paradigmatic for definitions of mixed variance. Generally, we regard the paper as a contribution to a more systematic understanding of the relation between higher-order and first-order inference rules.
Cite as
Stephan Alexander Spahn. Mendler Dialgebras and Recursion Schemes of Mixed Variance. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 15:1-15:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{spahn:LIPIcs.TYPES.2025.15,
author = {Spahn, Stephan Alexander},
title = {{Mendler Dialgebras and Recursion Schemes of Mixed Variance}},
booktitle = {31st International Conference on Types for Proofs and Programs (TYPES 2025)},
pages = {15:1--15:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-441-3},
ISSN = {1868-8969},
year = {2026},
volume = {384},
editor = {Nordvall Forsberg, Fredrik and McKinna, James},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.15},
URN = {urn:nbn:de:0030-drops-270338},
doi = {10.4230/LIPIcs.TYPES.2025.15},
annote = {Keywords: Mendler Algebra, Dinatural Transformation, Structured Recursion Scheme, Grothendieck Fibration, Higher-Order Abstract Syntax}
}