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/
Nakov, Georgi ;
Nordvall Forsberg, Fredrik
Quantitative Polynomial Functors
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}
}
