Document Open Access Logo

Quantitative Polynomial Functors (Early Ideas)

Authors Georgi Nakov, Fredrik Nordvall Forsberg

PDF
Thumbnail PDF

File

LIPIcs.CALCO.2021.22.pdf
  • Filesize: 0.53 MB
  • 5 pages

Document Identifiers

Author Details

Georgi Nakov
  • Department of Computer and Information Sciences, University of Strathclyde, UK
Fredrik Nordvall Forsberg
  • Department of Computer and Information Sciences, University of Strathclyde, UK

Cite AsGet BibTex

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)
https://doi.org/10.4230/LIPIcs.CALCO.2021.22

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Linear logic
Keywords
  • quantitative type theory
  • polynomial functors
  • inductive data types

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Michael Abbott, Thorsten Altenkirch, and Neil Ghani. Categories of containers. Lecture Notes in Computer Science, 2620:23-38, 2003. URL: https://doi.org/10.1007/3-540-36576-1_2.
  2. Andreas Abel and Jean-Philippe Bernardy. A unified view of modalities in type systems. Proceedings of the ACM on Programming Languages, 4(ICFP):1-28, 2020. URL: https://doi.org/10.1145/3408972.
  3. Robert Atkey. Syntax and Semantics of Quantitative Type Theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science - LICS '18, pages 56-65, New York, New York, USA, 2018. ACM Press. URL: https://doi.org/10.1145/3209108.3209189.
  4. Steve Awodey, Nicola Gambino, and Kristina Sojakova. Homotopy-initial algebras in type theory. Journal of the ACM, 63(6), 2017. Google Scholar
  5. P. N. Benton. A mixed linear and non-linear logic: Proofs, terms and models. In Lecture Notes in Computer Science, volume 933, pages 121-135. Springer, Berlin, Heidelberg, 1995. URL: https://doi.org/10.1007/BFb0022251.
  6. Iliano Cervesato and Frank Pfenning. A Linear Logical Framework. Information and Computation, 179(1):19-75, 2002. URL: https://doi.org/10.1006/inco.2001.2951.
  7. Peter Dybjer. Internal type theory. In Lecture Notes in Computer Science, volume 1158 LNCS, pages 120-134. Springer, Berlin, Heidelberg, 1996. URL: https://doi.org/10.1007/3-540-61780-9_66.
  8. Peng Fu, Kohei Kishida, and Peter Selinger. Linear Dependent Type Theory for Quantum Programming Languages: Extended Abstract. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 440-453. Association for Computing Machinery, 2020. URL: https://doi.org/10.1145/3373718.3394765.
  9. Claudio Hermida and Bart Jacobs. Structural Induction and Coinduction in a Fibrational Setting. Information and Computation, 145(2):107-152, 1998. URL: https://doi.org/10.1006/inco.1998.2725.
  10. Naohiko Hoshino. Linear Realizability. In Computer Science Logic, volume 4646 LNCS, pages 420-434. Springer Berlin Heidelberg, Berlin, Heidelberg, 2007. URL: https://doi.org/10.1007/978-3-540-74915-8_32.
  11. Neelakantan R. Krishnaswami, Pierre Pradic, and Nick Benton. Integrating Linear and Dependent Types. ACM SIGPLAN Notices, 50(1):17-30, 2015. URL: https://doi.org/10.1145/2775051.2676969.
  12. Conor McBride. I Got Plenty o' Nuttin'. In Lecture Notes in Computer Science, volume 9600, pages 207-233. Springer Verlag, 2016. URL: https://doi.org/10.1007/978-3-319-30936-1_12.
  13. Dominic Orchard, Vilem-Benjamin Liepelt, and Harley Eades III. Quantitative program reasoning with graded modal types. Proceedings of the ACM on Programming Languages, 3(ICFP):110:1-110:30, 2019. URL: https://doi.org/10.1145/3341714.
  14. Matthijs Vákár. In search of effectful dependent types. PhD thesis, University of Oxford, 2017. Google Scholar
  15. Jaap van Oosten. Realizability: an introduction to its categorical side. Elsevier, 2008. Google Scholar
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact