Quantitative polynomial functors

Nakov, Georgi and Nordvall Forsberg, Fredrik; (2022) Quantitative polynomial functors. In: 27th International Conference on Types for Proofs and Programs (TYPES 2021). Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 10:1--10:22. ISBN 9783959772549 (https://doi.org/10.4230/LIPIcs.TYPES.2021.10)

[thumbnail of Nakov-Forsberg-TYPES-2021-Quantitative-polynomial-functions]
Text. Filename: Nakov_Forsberg_TYPES_2021_Quantitative_polynomial_functions.pdf
Final Published Version
License: Creative Commons Attribution 4.0 logo

Download (907kB)| Preview


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.


Nakov, Georgi and Nordvall Forsberg, Fredrik ORCID logoORCID: https://orcid.org/0000-0001-6157-9288;