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.CALCO.2021.22
URN: urn:nbn:de:0030-drops-153774
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/15377/
Go to the corresponding LIPIcs Volume Portal

Nakov, Georgi ; Nordvall Forsberg, Fredrik

Quantitative Polynomial Functors (Early Ideas)

pdf-format:
LIPIcs-CALCO-2021-22.pdf (0.5 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.CALCO.2021.22,
  author =	{Nakov, Georgi and Nordvall Forsberg, Fredrik},
  title =	{{Quantitative Polynomial Functors}},
  booktitle =	{9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
  pages =	{22:1--22:5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-212-9},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{211},
  editor =	{Gadducci, Fabio and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/15377},
  URN =		{urn:nbn:de:0030-drops-153774},
  doi =		{10.4230/LIPIcs.CALCO.2021.22},
  annote =	{Keywords: quantitative type theory, polynomial functors, inductive data types}
}

Keywords: quantitative type theory, polynomial functors, inductive data types
Collection: 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)
Issue Date: 2021
Date of publication: 08.11.2021

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