Quantitative polynomial functors

Nakov, Georgi and Nordvall Forsberg, Fredrik; Basold, Henning and Cockx, Jesper and Ghilezan, Silvia, eds. (2022) Quantitative polynomial functors. In: 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics, LIPIcs, 239 . 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]
Preview
 Text. Filename: Nakov_Forsberg_TYPES_2021_Quantitative_polynomial_functions.pdf
Final Published Version
License: Creative Commons Attribution 4.0 logo
Download (907kB)| Preview

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.

ORCID iDs

Nakov, Georgi and Nordvall Forsberg, Fredrik ORCID logoORCID: https://orcid.org/0000-0001-6157-9288; Basold, Henning, Cockx, Jesper and Ghilezan, Silvia
CORE (COnnecting REpositories)