Quantitative polynomial functors

Georgi Nakov; Fredrik Nordvall Forsberg

doi:10.4230/LIPIcs.CALCO.2021.22

Quantitative polynomial functors

Georgi Nakov, Fredrik Nordvall Forsberg

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book

30 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 language	English
Title of host publication	9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)
Editors	Fabio Gadducci, Alexandra Silva
Place of Publication	Dagstuhl, Germany
Pages	22:1-22:5
Number of pages	5
DOIs	https://doi.org/10.4230/LIPIcs.CALCO.2021.22
Publication status	Published - 3 Sept 2021
Event	9th Conference on Algebra and Coalgebra in Computer Science, CALCO 2021 - Virtual, Salzburg, Austria Duration: 31 Aug 2021 → 3 Sept 2021

Publication series

Name	Leibniz International Proceedings in Informatics (LIPIcs)
Publisher	Schloss Dagstuhl
Volume	211
ISSN (Print)	1868-8969

Conference

Conference	9th Conference on Algebra and Coalgebra in Computer Science, CALCO 2021
Country/Territory	Austria
City	Virtual, Salzburg
Period	31/08/21 → 3/09/21

Keywords

inductive data types
polynomial functors
quantitative type theory

Access to Document

10.4230/LIPIcs.CALCO.2021.22Licence: CC BY 4.0

Nakov-Forsberg-CALCO-2021-Quantitative-polynomialFinal published version, 276 KBLicence: CC BY 4.0

Cite this

@inproceedings{ad9a7f81f10b4b65b871adc4e459ade0,

title = "Quantitative polynomial functors",

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.",

keywords = "inductive data types, polynomial functors, quantitative type theory",

author = "Georgi Nakov and Forsberg, {Fredrik Nordvall}",

year = "2021",

month = sep,

day = "3",

doi = "10.4230/LIPIcs.CALCO.2021.22",

language = "English",

isbn = "9783959772129",

series = "Leibniz International Proceedings in Informatics (LIPIcs)",

publisher = "Schloss Dagstuhl",

pages = "22:1--22:5",

editor = "Fabio Gadducci and Alexandra Silva",

booktitle = "9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)",

note = "9th Conference on Algebra and Coalgebra in Computer Science, CALCO 2021 ; Conference date: 31-08-2021 Through 03-09-2021",

}

Nakov, G & Forsberg, FN 2021, Quantitative polynomial functors. in F Gadducci & A Silva (eds), 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol. 211, Dagstuhl, Germany, pp. 22:1-22:5, 9th Conference on Algebra and Coalgebra in Computer Science, CALCO 2021, Virtual, Salzburg, Austria, 31/08/21. https://doi.org/10.4230/LIPIcs.CALCO.2021.22

Quantitative polynomial functors. / Nakov, Georgi ; Forsberg, Fredrik Nordvall.
9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). ed. / Fabio Gadducci; Alexandra Silva. Dagstuhl, Germany, 2021. p. 22:1-22:5 (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 211).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book

TY - GEN

T1 - Quantitative polynomial functors

AU - Nakov, Georgi

AU - Forsberg, Fredrik Nordvall

PY - 2021/9/3

Y1 - 2021/9/3

N2 - 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.

AB - 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.

KW - inductive data types

KW - polynomial functors

KW - quantitative type theory

UR - http://www.scopus.com/inward/record.url?scp=85120636615&partnerID=8YFLogxK

UR - https://www.coalg.org/calco-mfps2021/

U2 - 10.4230/LIPIcs.CALCO.2021.22

DO - 10.4230/LIPIcs.CALCO.2021.22

M3 - Conference contribution book

AN - SCOPUS:85120636615

SN - 9783959772129

T3 - Leibniz International Proceedings in Informatics (LIPIcs)

SP - 22:1-22:5

BT - 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)

A2 - Gadducci, Fabio

A2 - Silva, Alexandra

CY - Dagstuhl, Germany

T2 - 9th Conference on Algebra and Coalgebra in Computer Science, CALCO 2021

Y2 - 31 August 2021 through 3 September 2021

ER -

Quantitative polynomial functors

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Quantitative polynomial functors

Cite this