Document Open Access Logo

Dialectica Comonads (Invited Talk)

Author Valeria de Paiva

PDF
Thumbnail PDF

File

LIPIcs.CALCO.2021.3.pdf
  • Filesize: 0.65 MB
  • 13 pages

Document Identifiers

Author Details

Valeria de Paiva
  • Topos Institute, Berkeley, CA, USA

Funding

  • de Paiva, Valeria: Research supported by AFOSR grant FA9550-20-10348.

Acknowledgements

I would like to thank Fabio Gadducci and Alexandra Silva for the invitation to speak at CALCO2021. Thinking about the CALCO community and how it influences my work was much more fun than I had expected.

Cite AsGet BibTex

Valeria de Paiva. Dialectica Comonads (Invited Talk). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 3:1-3:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CALCO.2021.3

Abstract

Dialectica categories are interesting categorical models of Linear Logic which preserve the differences between linear connectives that the logic is supposed to make, unlike some of the most traditional models like coherence spaces. They arise from the categorical modelling of Gödel’s Dialectica interpretation and seem to be having a revival: connections between Dialectica constructions and containers, lenses and polynomials have been described recently in the literature. In this note I will recap the basic Dialectica constructions and then go on to describe the less well-known interplay of comonads, coalgebras and comonoids that characterizes the composite functor standing for the "of course!" operator in dialectica categories. This composition of comonads evokes some work on stateful games by Laird and others, also discussed in the setting of Reddy’s system LLMS (Linear Logic Model of State).

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
Keywords
  • Dialectica categories
  • Linear logic
  • Comonads

Metrics

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

References

  1. Paul André Melliès. Categorical semantics of linear logic. In In: Interactive Models of Computation and Program Behaviour, Panoramas et Synthèses 27, Société Mathématique de France 1–196, 2009. Google Scholar
  2. Andrew Barber and Gordon Plotkin. Dual intuitionistic linear logic. University of Edinburgh, Department of Computer Science, Laboratory for …, 1996. Google Scholar
  3. Jon Beck. Distributive laws. In B. Eckmann, editor, Seminar on Triples and Categorical Homology Theory, pages 119-140, Berlin, Heidelberg, 1969. Springer Berlin Heidelberg. Google Scholar
  4. Nick Benton, Gavin Bierman, Valeria De Paiva, and Martin Hyland. A term calculus for intuitionistic linear logic. In International Conference on Typed Lambda Calculi and Applications, pages 75-90. Springer, 1993. Google Scholar
  5. P. N. Benton. A mixed linear and non-linear logic: Proofs, terms and models. In Leszek Pacholski and Jerzy Tiuryn, editors, Computer Science Logic, pages 121-135, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg. Google Scholar
  6. Gavin M Bierman. What is a categorical model of intuitionistic linear logic? In International Conference on Typed Lambda Calculi and Applications, pages 78-93. Springer, 1995. Google Scholar
  7. Martin Churchill and James Laird. A logic of sequentiality. In International Workshop on Computer Science Logic, pages 215-229. Springer, 2010. Google Scholar
  8. Marcelo da S Corrêa, Edward H Haeusler, and Valeria CV de Paiva. A dialectica model of state. In CATS’96, Computing: The Australian Theory Symposium Proceedings, pages 11-12, 1996. Google Scholar
  9. Valeria de Paiva. The dialectica categories. Categories in Computer Science and Logic, 92:47-62, 1989. Google Scholar
  10. Valeria De Paiva. A dialectica model of the lambek calculus. In AMSTERDAM COLLOQUIUM, 1991. Citeseer, 1991. Google Scholar
  11. Valeria De Paiva. Linear logic model of state revisited. Logic Journal of the IGPL, 22(5):791-804, 2014. Google Scholar
  12. Valeria de Paiva, Rajeev Goré, and Michael Mendler. Modalities in constructive logics and type theories, 2004. Google Scholar
  13. Valeria de Paiva and Brigitte Pientka. Intuitionistic modal logic and applications (IMLA 2008). Information and computation (Print), 209(12), 2011. Google Scholar
  14. Valeria Correa Vaz de Paiva. The dialectica categories. Technical report, University of Cambridge, Computer Laboratory, Technical Report 213, 1991. URL: https://128.232.0.20/techreports/UCAM-CL-TR-213.pdf.
  15. Valeria CV De Paiva. A dialectica-like model of linear logic. In Category Theory and Computer Science, pages 341-356. Springer, 1989. Google Scholar
  16. Harley Eades and Valeria de Paiva. Multiple conclusion linear logic: Cut elimination and more. In Sergei Artemov and Anil Nerode, editors, Logical Foundations of Computer Science, pages 90-105, Cham, 2016. Springer International Publishing. Google Scholar
  17. Jean-Yves Girard and Yves Lafont. Linear logic and lazy computation. In International Joint Conference on Theory and Practice of Software Development, pages 52-66. Springer, 1987. Google Scholar
  18. J.M.E. Hyland. Proof theory in the abstract. Annals of Pure and Applied Logic, 114(1):43-78, 2002. Troelstra Festschrift. URL: https://doi.org/10.1016/S0168-0072(01)00075-6.
  19. Martin Hyland and Valeria De Paiva. Full intuitionistic linear logic. Annals of Pure and Applied Logic, 64(3):273-291, 1993. Google Scholar
  20. Martin Hyland and Andrea Schalk. Glueing and orthogonality for models of linear logic. Theoretical computer science, 294(1-2):183-231, 2003. Google Scholar
  21. Ulrich Kohlenbach. Applied proof theory: proof interpretations and their use in mathematics. Springer Science & Business Media, 2008. Google Scholar
  22. Yves Lafont and Thomas Streicher. Games semantics for linear logic. In Proceedings 1991 Sixth Annual IEEE Symposium on Logic in Computer Science, pages 43-44. IEEE Computer Society, 1991. Google Scholar
  23. Maria Emilia Maietti, Paola Maneggia, Valeria De Paiva, and Eike Ritter. Relating categorical semantics for intuitionistic linear logic. Applied categorical structures, 13(1):1-36, 2005. Google Scholar
  24. Vaughan Pratt. Chu spaces. School on Category Theory and Applications (Coimbra, 1999), 21:39-100, 1999. Google Scholar
  25. Uday S. Reddy. A linear logic model of state. Manuscript, 1993. Google Scholar
  26. Christian Retoré. Pomset logic: A non-commutative extension of classical linear logic. In Philippe de Groote and J. Roger Hindley, editors, Typed Lambda Calculi and Applications, pages 300-318, Berlin, Heidelberg, 1997. Springer Berlin Heidelberg. Google Scholar
  27. Christian Retoré. Pomset logic: a logical and grammatical alternative to the lambek calculus, 2020. URL: http://arxiv.org/abs/2001.02155.
  28. R.A.G. Seely. Linear logic, *-autonomous categories and cofree coalgebras. In Categories in Computer Science and Logic, pages 371-382. American Mathematical Society, 1989. Google Scholar
  29. Sergey Slavnov. On noncommutative extensions of linear logic. arXiv preprint arXiv:1703.10092, 2017. Google Scholar
  30. Charles Stewart, Valeria de Paiva, and Natasha Alechina. Intuitionistic modal logic: a 15-year retrospective. Journal of Logic and Computation, 2018. Google Scholar
  31. Ross Street. The formal theory of monads. Journal of Pure and Applied Algebra, 2(2):149-168, 1972. URL: https://doi.org/10.1016/0022-4049(72)90019-9.
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact