Search Results

Documents authored by van den Berg, Benno

Document
DOI: 10.4230/LIPIcs.FSCD.2026.21
Constructing (Co)inductive Types via Large Sizes

Authors: Bastiaan Laarakker, Daniël Otten, and Benno van den Berg

Published in: LIPIcs, Volume 378, 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)

Abstract
To ensure decidability and consistency of its type theory, a proof assistant should only accept terminating recursive functions and productive corecursive functions. Most proof assistants enforce this through syntactic conditions, which can be restrictive and non-modular. Sized types are a type-based alternative where (co)inductive types are annotated with additional size information. Well-founded induction on sizes can then be used to prove termination and productivity. An implementation of sized types exists in Agda, but it is currently inconsistent due to the addition of a largest size. We investigate an alternative approach, where intensional type theory is extended with a large type of sizes and parametric quantifiers over sizes. We show that inductive and coinductive types can be constructed in this theory, which improves on earlier work where this was only possible for the finitely-branching inductive types. The consistency of the theory is justified by an impredicative realisability model, which interprets the type of sizes as an uncountable ordinal.
Cite as

Bastiaan Laarakker, Daniël Otten, and Benno van den Berg. Constructing (Co)inductive Types via Large Sizes. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 21:1-21:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{laarakker_et_al:LIPIcs.FSCD.2026.21,
  author =	{Laarakker, Bastiaan and Otten, Dani\"{e}l and van den Berg, Benno},
  title =	{{Constructing (Co)inductive Types via Large Sizes}},
  booktitle =	{11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
  pages =	{21:1--21:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-433-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{378},
  editor =	{Pfenning, Frank},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.21},
  URN =		{urn:nbn:de:0030-drops-263714},
  doi =		{10.4230/LIPIcs.FSCD.2026.21},
  annote =	{Keywords: Sized Types, Parametricity, Realisability, Impredicativity, Constructive Ordinals, (Co)inductive Types}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.TYPES.2024
LIPIcs, Volume 336, TYPES 2024, Complete Volume

Authors: Rasmus Ejlers Møgelberg and Benno van den Berg

Published in: LIPIcs, Volume 336, 30th International Conference on Types for Proofs and Programs (TYPES 2024)

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
DOI: 10.4230/LIPIcs.TYPES.2024.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Rasmus Ejlers Møgelberg and Benno van den Berg

Published in: LIPIcs, Volume 336, 30th International Conference on Types for Proofs and Programs (TYPES 2024)

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
Complete Volume
DOI: 10.4230/LIPIcs.TYPES.2023
LIPIcs, Volume 303, TYPES 2023, Complete Volume

Authors: Delia Kesner, Eduardo Hermo Reyes, and Benno van den Berg

Published in: LIPIcs, Volume 303, 29th International Conference on Types for Proofs and Programs (TYPES 2023)

Abstract
LIPIcs, Volume 303, TYPES 2023, Complete Volume
Cite as

29th International Conference on Types for Proofs and Programs (TYPES 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 303, pp. 1-138, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Proceedings{kesner_et_al:LIPIcs.TYPES.2023,
  title =	{{LIPIcs, Volume 303, TYPES 2023, Complete Volume}},
  booktitle =	{29th International Conference on Types for Proofs and Programs (TYPES 2023)},
  pages =	{1--138},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-332-4},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{303},
  editor =	{Kesner, Delia and Reyes, Eduardo Hermo 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.2023},
  URN =		{urn:nbn:de:0030-drops-204778},
  doi =		{10.4230/LIPIcs.TYPES.2023},
  annote =	{Keywords: LIPIcs, Volume 303, TYPES 2023, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.TYPES.2023.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Delia Kesner, Eduardo Hermo Reyes, and Benno van den Berg

Published in: LIPIcs, Volume 303, 29th International Conference on Types for Proofs and Programs (TYPES 2023)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

29th International Conference on Types for Proofs and Programs (TYPES 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 303, pp. 0:i-0:viii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{kesner_et_al:LIPIcs.TYPES.2023.0,
  author =	{Kesner, Delia and Reyes, Eduardo Hermo and van den Berg, Benno},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{29th International Conference on Types for Proofs and Programs (TYPES 2023)},
  pages =	{0:i--0:viii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-332-4},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{303},
  editor =	{Kesner, Delia and Reyes, Eduardo Hermo 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.2023.0},
  URN =		{urn:nbn:de:0030-drops-204787},
  doi =		{10.4230/LIPIcs.TYPES.2023.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.CSL.2024.44
Conservativity of Type Theory over Higher-Order Arithmetic

Authors: Daniël Otten and Benno van den Berg

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract
We investigate how much type theory can prove about the natural numbers. A classical result in this area shows that dependent type theory without any universes is conservative over Heyting Arithmetic (HA). We build on this result by showing that type theories with one level of impredicative universes are conservative over Higher-order Heyting Arithmetic (HAH). This result clearly depends on the specific type theory in question, however, we show that the interpretation of logic also plays a major role. For proof-irrelevant interpretations, we will see that strong versions of type theory prove exactly the same higher-order arithmetical formulas as HAH. Conversely, for proof-relevant interpretations, they prove different second-order arithmetical formulas than HAH, while still proving exactly the same first-order arithmetical formulas. Along the way, we investigate the various interpretations of logic in type theory, and to what extent dependent type theories can be seen as extensions of higher-order logic. We apply our results by proving a De Jongh’s theorem for type theory.
Cite as

Daniël Otten and Benno van den Berg. Conservativity of Type Theory over Higher-Order Arithmetic. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 44:1-44:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{otten_et_al:LIPIcs.CSL.2024.44,
  author =	{Otten, Dani\"{e}l and van den Berg, Benno},
  title =	{{Conservativity of Type Theory over Higher-Order Arithmetic}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{44:1--44:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.44},
  URN =		{urn:nbn:de:0030-drops-196873},
  doi =		{10.4230/LIPIcs.CSL.2024.44},
  annote =	{Keywords: Conservativity, Arithmetic, Realizability, Calculus of Inductive Constructions}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact