Volume
LIPIcs, Volume 336
30th International Conference on Types for Proofs and Programs (TYPES 2024)
Event
TYPES 2024, June 10-14, 2024, Copenhagen, DenmarkEditors
Publication Details
- published at: 2025-07-03
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-376-8
- DBLP: db/conf/types/types2024
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 336, TYPES 2024, Complete Volume
Abstract
LIPIcs, Volume 336, TYPES 2024, Complete Volume
Cite as
30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 1-190, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Proceedings{mogelberg_et_al:LIPIcs.TYPES.2024,
title = {{LIPIcs, Volume 336, TYPES 2024, Complete Volume}},
booktitle = {30th International Conference on Types for Proofs and Programs (TYPES 2024)},
pages = {1--190},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-376-8},
ISSN = {1868-8969},
year = {2025},
volume = {336},
editor = {M{\o}gelberg, Rasmus Ejlers and van den Berg, Benno},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024},
URN = {urn:nbn:de:0030-drops-237954},
doi = {10.4230/LIPIcs.TYPES.2024},
annote = {Keywords: LIPIcs, Volume 336, TYPES 2024, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{mogelberg_et_al:LIPIcs.TYPES.2024.0,
author = {M{\o}gelberg, Rasmus Ejlers and van den Berg, Benno},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {30th International Conference on Types for Proofs and Programs (TYPES 2024)},
pages = {0:i--0:xii},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-376-8},
ISSN = {1868-8969},
year = {2025},
volume = {336},
editor = {M{\o}gelberg, Rasmus Ejlers and van den Berg, Benno},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.0},
URN = {urn:nbn:de:0030-drops-237837},
doi = {10.4230/LIPIcs.TYPES.2024.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Formalizing Equivalences Without Tears
Abstract
This expository note describes two convenient techniques in the context of homotopy type theory for proving - and formalizing - that a given map is an equivalence. The first technique decomposes the map as a series of basic equivalences, while the second refines this approach using the 3-for-2 property of equivalences. The techniques are illustrated by proving a basic result in synthetic homotopy theory.
Cite as
Tom de Jong. Formalizing Equivalences Without Tears. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 1:1-1:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{dejong:LIPIcs.TYPES.2024.1,
author = {de Jong, Tom},
title = {{Formalizing Equivalences Without Tears}},
booktitle = {30th International Conference on Types for Proofs and Programs (TYPES 2024)},
pages = {1:1--1:6},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-376-8},
ISSN = {1868-8969},
year = {2025},
volume = {336},
editor = {M{\o}gelberg, Rasmus Ejlers and van den Berg, Benno},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.1},
URN = {urn:nbn:de:0030-drops-233632},
doi = {10.4230/LIPIcs.TYPES.2024.1},
annote = {Keywords: 3-for-2 property, 2-out-of-3 property, definitional equality, equivalence, formalization of mathematics, synthetic homotopy theory, type theory}
}
Document
Constructive Substitutes for Kőnig’s Lemma
Abstract
We propose weaker but constructively provable variants of the contrapositive of Kőnig’s lemma. We derive those from a generalization of the FAN theorem for inductive bars to inductive covers, for which we give a concise proof. We compare the positive, negative and sequential characterizations of covers and bars in classical and constructive contexts, giving precise accounts of the role played by the axioms of excluded middle and dependent choice. As an application, we discuss some examples where the use of Kőnig’s lemma can be replaced by one of our weaker variants to obtain fully constructive accounts of results or proofs that could otherwise appear as inherently classical.
Cite as
Dominique Larchey-Wendling. Constructive Substitutes for Kőnig’s Lemma. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 2:1-2:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{larcheywendling:LIPIcs.TYPES.2024.2,
author = {Larchey-Wendling, Dominique},
title = {{Constructive Substitutes for K\H{o}nig’s Lemma}},
booktitle = {30th International Conference on Types for Proofs and Programs (TYPES 2024)},
pages = {2:1--2:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-376-8},
ISSN = {1868-8969},
year = {2025},
volume = {336},
editor = {M{\o}gelberg, Rasmus Ejlers and van den Berg, Benno},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.2},
URN = {urn:nbn:de:0030-drops-233644},
doi = {10.4230/LIPIcs.TYPES.2024.2},
annote = {Keywords: K\H{o}nig’s lemma, FAN theorem, constructive mathematics, inductive covers, inductive bars, almost full relations, inductive type theory, Coq}
}
Document
A Foundation for Synthetic Stone Duality
Abstract
The language of homotopy type theory has proved to be an appropriate internal language for various higher toposes, for example for the Zariski topos in Synthetic Algebraic Geometry. This paper aims to do the same for the higher topos of light condensed anima of Dustin Clausen and Peter Scholze. This seems to be an appropriate setting for synthetic topology in the style of Martín Escardó.
We use homotopy type theory extended with 4 axioms. We prove Markov’s principle, LLPO and the negation of WLPO. Then we define a type of open propositions, inducing a topology on any type such that any map is continuous. We give a synthetic definition of second countable Stone and compact Hausdorff spaces, and show that their induced topologies are as expected. This means that any map from e.g. the unit interval 𝕀 to itself is continuous in the usual epsilon-delta sense.
With the usual definition of cohomology in homotopy type theory, we show that H¹(S,ℤ) = 0 for S Stone and that H¹(X,ℤ) for X compact Hausdorff can be computed using Čech cohomology. We use this to prove H¹(𝕀¹,ℤ) = 0 and H¹(𝕊¹,ℤ) = ℤ where 𝕊¹ is the set ℝ/ℤ. As an application, we give a synthetic proof of Brouwer’s fixed-point theorem.
Cite as
Felix Cherubini, Thierry Coquand, Freek Geerligs, and Hugo Moeneclaey. A Foundation for Synthetic Stone Duality. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 3:1-3:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{cherubini_et_al:LIPIcs.TYPES.2024.3,
author = {Cherubini, Felix and Coquand, Thierry and Geerligs, Freek and Moeneclaey, Hugo},
title = {{A Foundation for Synthetic Stone Duality}},
booktitle = {30th International Conference on Types for Proofs and Programs (TYPES 2024)},
pages = {3:1--3:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-376-8},
ISSN = {1868-8969},
year = {2025},
volume = {336},
editor = {M{\o}gelberg, Rasmus Ejlers and van den Berg, Benno},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.3},
URN = {urn:nbn:de:0030-drops-233659},
doi = {10.4230/LIPIcs.TYPES.2024.3},
annote = {Keywords: Homotopy Type Theory, Synthetic Topology, Cohomology}
}
Document
Separating Terms by Means of Multi Types, Coinductively
Abstract
Intersection type systems, as adequate models of the λ-calculus, induce an equational theory on terms, that we refer to as type equivalence. We give a new proof technique to coinductively characterize type equivalence. To do so, we explore a simple setting, namely weak head type equivalence, which is the equational theory induced by a weak head non-idempotent intersection type system.
We prove a folklore result: weak head type equivalence coincides with Sangiorgi’s normal form bisimilarity. What is new in our development is that we only rely on coinductive program equivalences, bypassing the need to introduce term approximants, which were used in previous works characterizing type equivalence.
The crucial part of this characterization is to show that type equivalent terms are normal form bisimilar: we do so by constructing shape typings that can only type terms of a specific normal form structure. Shape typings are a light form of principal types, a technique often used in intersection types to generate from one or few principal typing all possible typings of a term.
Cite as
Adrienne Lancelot. Separating Terms by Means of Multi Types, Coinductively. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 4:1-4:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{lancelot:LIPIcs.TYPES.2024.4,
author = {Lancelot, Adrienne},
title = {{Separating Terms by Means of Multi Types, Coinductively}},
booktitle = {30th International Conference on Types for Proofs and Programs (TYPES 2024)},
pages = {4:1--4:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-376-8},
ISSN = {1868-8969},
year = {2025},
volume = {336},
editor = {M{\o}gelberg, Rasmus Ejlers and van den Berg, Benno},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.4},
URN = {urn:nbn:de:0030-drops-233660},
doi = {10.4230/LIPIcs.TYPES.2024.4},
annote = {Keywords: lambda calculus, intersection types, program equivalence}
}
Document
Implementing a Type Theory with Observational Equality, Using Normalisation by Evaluation
Abstract
We report on an experimental implementation in Haskell of a dependent type theory featuring an observational equality type, based on Pujet et al.’s CCobs. We use normalisation by evaluation to produce an efficient normalisation function, which is used to implement a bidirectional type checker. To allow for greater expressivity, we extend the core CCobs calculus with quotient types and inductive types. To make the system usable, we explore various proof-assistant features, notably a rudimentary version of a "hole" system similar to Agda’s. While rather crude, this experience should inform other, more substantial implementation efforts of observational equality.
Cite as
Matthew Sirman, Meven Lennon-Bertrand, and Neel Krishnaswami. Implementing a Type Theory with Observational Equality, Using Normalisation by Evaluation. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 5:1-5:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{sirman_et_al:LIPIcs.TYPES.2024.5,
author = {Sirman, Matthew and Lennon-Bertrand, Meven and Krishnaswami, Neel},
title = {{Implementing a Type Theory with Observational Equality, Using Normalisation by Evaluation}},
booktitle = {30th International Conference on Types for Proofs and Programs (TYPES 2024)},
pages = {5:1--5:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-376-8},
ISSN = {1868-8969},
year = {2025},
volume = {336},
editor = {M{\o}gelberg, Rasmus Ejlers and van den Berg, Benno},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.5},
URN = {urn:nbn:de:0030-drops-233673},
doi = {10.4230/LIPIcs.TYPES.2024.5},
annote = {Keywords: Dependent type theory, Bidirectional typing, Observational equality, Normalisation by evaluation}
}
Document
Data Types with Symmetries via Action Containers
Abstract
We study two kinds of containers for data types with symmetries in homotopy type theory, and clarify their relationship by introducing the intermediate notion of action containers. Quotient containers are set-valued containers with groups of permissible permutations of positions, interpreted as (possibly non-finitary) analytic functors on the category of sets. Symmetric containers encode symmetries in a groupoid of shapes, and are interpreted accordingly as polynomial functors on the 2-category of groupoids.
Action containers are endowed with groups that act on their positions, with morphisms preserving the actions. We show that, as a category, action containers are equivalent to the free coproduct completion of a category of group actions. We derive that they model non-inductive single-variable strictly positive types in the sense of Abbott et al.: The category of action containers is closed under arbitrary (co)products and exponentiation with constants. We equip this category with the structure of a locally groupoidal 2-category, and prove that it locally embeds into the 2-category of symmetric containers. This follows from the embedding of a 2-category of groups into the 2-category of groupoids, extending the delooping construction.
Cite as
Philipp Joram and Niccolò Veltri. Data Types with Symmetries via Action Containers. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 6:1-6:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{joram_et_al:LIPIcs.TYPES.2024.6,
author = {Joram, Philipp and Veltri, Niccol\`{o}},
title = {{Data Types with Symmetries via Action Containers}},
booktitle = {30th International Conference on Types for Proofs and Programs (TYPES 2024)},
pages = {6:1--6:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-376-8},
ISSN = {1868-8969},
year = {2025},
volume = {336},
editor = {M{\o}gelberg, Rasmus Ejlers and van den Berg, Benno},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.6},
URN = {urn:nbn:de:0030-drops-233681},
doi = {10.4230/LIPIcs.TYPES.2024.6},
annote = {Keywords: Containers, Homotopy Type Theory, Agda, 2-categories}
}
Document
Synthetic 1-Categories in Directed Type Theory
Abstract
The field of directed type theory seeks to design type theories capable of reasoning synthetically about (higher) categories, by generalizing the symmetric identity types of Martin-Löf Type Theory to asymmetric hom-types. We articulate the directed type theory of the category model, with appropriate modalities for keeping track of variances and a powerful directed-J rule capable of proving results about arbitrary terms of hom-types; we put this rule to use in making several constructions in synthetic 1-category theory. Because this theory is expressed entirely in terms of generalized algebraic theories, we know automatically that this directed type theory admits a syntax model.
Cite as
Jacob Neumann and Thorsten Altenkirch. Synthetic 1-Categories in Directed Type Theory. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 7:1-7:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{neumann_et_al:LIPIcs.TYPES.2024.7,
author = {Neumann, Jacob and Altenkirch, Thorsten},
title = {{Synthetic 1-Categories in Directed Type Theory}},
booktitle = {30th International Conference on Types for Proofs and Programs (TYPES 2024)},
pages = {7:1--7:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-376-8},
ISSN = {1868-8969},
year = {2025},
volume = {336},
editor = {M{\o}gelberg, Rasmus Ejlers and van den Berg, Benno},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.7},
URN = {urn:nbn:de:0030-drops-233694},
doi = {10.4230/LIPIcs.TYPES.2024.7},
annote = {Keywords: Semantics, directed type theory, homotopy type theory, category theory, generalized algebraic theories}
}
Document
Effective Kan Fibrations for W-Types in Homotopy Type Theory
Abstract
We investigate effective Kan fibrations in the context of the semantics of Homotopy Type Theory (HoTT). Effective Kan fibrations were proposed by Benno van den Berg and Eric Faber as constructive alternatives to classical Kan fibrations for modeling HoTT. Our work specifically explores their interaction with W-types in HoTT, which are inductive types representing well-founded trees, and extends this exploration to variants such as M-types. By using the categorical properties of W-types, we show that effective Kan fibrations model them. Additionally, we examine the behavior of quotient maps and discuss that certain cases can also be classified as effective Kan fibrations.
Cite as
Shinichiro Tanaka. Effective Kan Fibrations for W-Types in Homotopy Type Theory. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{tanaka:LIPIcs.TYPES.2024.8,
author = {Tanaka, Shinichiro},
title = {{Effective Kan Fibrations for W-Types in Homotopy Type Theory}},
booktitle = {30th International Conference on Types for Proofs and Programs (TYPES 2024)},
pages = {8:1--8:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-376-8},
ISSN = {1868-8969},
year = {2025},
volume = {336},
editor = {M{\o}gelberg, Rasmus Ejlers and van den Berg, Benno},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.8},
URN = {urn:nbn:de:0030-drops-233707},
doi = {10.4230/LIPIcs.TYPES.2024.8},
annote = {Keywords: Homotopy Type Theory, Effective Kan Fibrations, W-types}
}
Document
Complexity of Cubical Cofibration Logics I: coNP-Complete Examples
Abstract
We provide a comprehensive classification of the cofibration entailment problem, COFENT, for the cofibration logics of various cubical type theories in use today. The problem COFENT arose from the need of cubical proof assistants to automate reasoning about cubical complexes included in an n-dimensional hypercube. Intuitively, it asks: given logical descriptions of two such complexes, is one a subcomplex of the other? We show that the common variants of COFENT are coNP-complete.
Cite as
Robert Rose and Daniel R. Licata. Complexity of Cubical Cofibration Logics I: coNP-Complete Examples. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 9:1-9:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{rose_et_al:LIPIcs.TYPES.2024.9,
author = {Rose, Robert and Licata, Daniel R.},
title = {{Complexity of Cubical Cofibration Logics I: coNP-Complete Examples}},
booktitle = {30th International Conference on Types for Proofs and Programs (TYPES 2024)},
pages = {9:1--9:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-376-8},
ISSN = {1868-8969},
year = {2025},
volume = {336},
editor = {M{\o}gelberg, Rasmus Ejlers and van den Berg, Benno},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.9},
URN = {urn:nbn:de:0030-drops-233711},
doi = {10.4230/LIPIcs.TYPES.2024.9},
annote = {Keywords: cubical sets, internal language, intuitionistic logic, dependent type theory, homotopy type theory, decision procedures}
}