DROPS

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}
}

Search Results

Documents authored by Laarakker, Bastiaan

Constructing (Co)inductive Types via Large Sizes

Abstract

Cite as

Thanks for your feedback!

Could not send message