Search Results

Documents authored by Nakov, Georgi


Document
Quantitative Polynomial Functors

Authors: Georgi Nakov and Fredrik Nordvall Forsberg

Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)


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.

Cite as

Georgi Nakov and Fredrik Nordvall Forsberg. Quantitative Polynomial Functors. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 10:1-10:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{nakov_et_al:LIPIcs.TYPES.2021.10,
  author =	{Nakov, Georgi and Nordvall Forsberg, Fredrik},
  title =	{{Quantitative Polynomial Functors}},
  booktitle =	{27th International Conference on Types for Proofs and Programs (TYPES 2021)},
  pages =	{10:1--10:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-254-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{239},
  editor =	{Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.10},
  URN =		{urn:nbn:de:0030-drops-167795},
  doi =		{10.4230/LIPIcs.TYPES.2021.10},
  annote =	{Keywords: quantitative type theory, polynomial functors, inductive data types}
}
Document
Early Ideas
Quantitative Polynomial Functors (Early Ideas)

Authors: Georgi Nakov and Fredrik Nordvall Forsberg

Published in: LIPIcs, Volume 211, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)


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.

Cite as

Georgi Nakov and Fredrik Nordvall Forsberg. Quantitative Polynomial Functors (Early Ideas). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 22:1-22:5, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{nakov_et_al:LIPIcs.CALCO.2021.22,
  author =	{Nakov, Georgi and Nordvall Forsberg, Fredrik},
  title =	{{Quantitative Polynomial Functors}},
  booktitle =	{9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
  pages =	{22:1--22:5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-212-9},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{211},
  editor =	{Gadducci, Fabio and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.22},
  URN =		{urn:nbn:de:0030-drops-153774},
  doi =		{10.4230/LIPIcs.CALCO.2021.22},
  annote =	{Keywords: quantitative type theory, polynomial functors, inductive data types}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail