2026-08-15T23:19:07Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16779 2024-03-06T10:58:15Z ddc:004 open_access

Quantitative Polynomial Functors Nakov, Georgi Nordvall Forsberg, Fredrik quantitative type theory polynomial functors inductive data types 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Georgi Nakov and Fredrik Nordvall Forsberg 2022 Is Part Of LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2021.10 urn:nbn:de:0030-drops-167795 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.10 eng https://creativecommons.org/licenses/by/4.0/legalcode