License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2021.10
URN: urn:nbn:de:0030-drops-167795
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16779/
Go to the corresponding LIPIcs Volume Portal


Nakov, Georgi ; Nordvall Forsberg, Fredrik

Quantitative Polynomial Functors

pdf-format:
LIPIcs-TYPES-2021-10.pdf (0.9 MB)


Abstract

We investigate containers and polynomial functors in Quantitative Type Theory, and give initial algebra semantics of inductive data types in the presence of linearity. We show that reasoning by induction is supported, and equivalent to initiality, also in the linear setting.

BibTeX - Entry

@InProceedings{nakov_et_al:LIPIcs.TYPES.2021.10,
  author =	{Nakov, Georgi and Nordvall Forsberg, Fredrik},
  title =	{{Quantitative Polynomial Functors}},
  booktitle =	{27th International Conference on Types for Proofs and Programs (TYPES 2021)},
  pages =	{10:1--10:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-254-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{239},
  editor =	{Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16779},
  URN =		{urn:nbn:de:0030-drops-167795},
  doi =		{10.4230/LIPIcs.TYPES.2021.10},
  annote =	{Keywords: quantitative type theory, polynomial functors, inductive data types}
}

Keywords: quantitative type theory, polynomial functors, inductive data types
Collection: 27th International Conference on Types for Proofs and Programs (TYPES 2021)
Issue Date: 2022
Date of publication: 04.08.2022
Supplementary Material: Software (Idris 2 Formalisation): https://github.com/g-nakov/quantitative-poly archived at: https://archive.softwareheritage.org/swh:1:dir:ae7679e3704d07ffa7732029c7c9f0f68abf1271


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI