nakov_quantitative_2022:
  type: article
  title: Quantitative {Polynomial} {Functors}
  author:
  - Nakov, Georgi
  - Nordvall Forsberg, Fredrik
  date: 2022
  page-range: 10:1–10:22
  url:
    value: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.10
    date: 2024-11-13
  serial-number:
    doi: 10.4230/LIPIcs.TYPES.2021.10
  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.
  parent:
    type: proceedings
    title: 27th {International} {Conference} on {Types} for {Proofs} and {Programs} ({TYPES} 2021)
    publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik