Quantitative polynomial functors

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

2 Downloads (Pure)

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.
Original languageEnglish
Title of host publication27th International Conference on Types for Proofs and Programs (TYPES 2021)
EditorsHenning Basold, Jesper Cockx, Silvia Ghilezan
Place of PublicationDagstuhl, Germany
Pages10:1--10:22
Number of pages22
Volume239
ISBN (Electronic)9783959772549
DOIs
Publication statusPublished - 4 Aug 2022

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume239
ISSN (Print)1868-8969

Keywords

  • quantitative type theory
  • polynomial functors
  • inductive data types
  • computational theory
  • type theory
  • linear logic

Fingerprint

Dive into the research topics of 'Quantitative polynomial functors'. Together they form a unique fingerprint.
  • Quantitative polynomial functors

    Nakov, G. & Forsberg, F. N., 3 Sep 2021, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Gadducci, F. & Silva, A. (eds.). Dagstuhl, Germany, p. 22:1-22:5 5 p. (Leibniz International Proceedings in Informatics (LIPIcs); vol. 211).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution book

    Open Access
    File
    4 Downloads (Pure)

Cite this