Document Open Access Logo

Dialectica Categories and Games with Bidding

Author Jules Hedges

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2014.89.pdf
  • Filesize: 0.48 MB
  • 22 pages

Document Identifiers

Subject Classification

Keywords
  • Linear logic
  • Dialectica categories
  • categorical semantics
  • model theory
  • game semantics
  • dependent types
  • functional interpretations

Metrics

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

Abstract

This paper presents a construction which transforms categorical models of additive-free propositional linear logic, closely based on de Paiva's dialectica categories and Oliva's functional interpretations of classical linear logic. The construction is defined using dependent type theory, which proves to be a useful tool for reasoning about dialectica categories. Abstractly, we have a closure operator on the class of models: it preserves soundness and completeness and has a monad-like structure. When applied to categories of games we obtain 'games with bidding', which are hybrids of dialectica and game models, and we prove completeness theorems for two specific such models.

Cite As Get BibTex

Jules Hedges. Dialectica Categories and Games with Bidding. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 89-110, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.TYPES.2014.89

Author Details

Jules Hedges

References

  1. Jeremy Avigad and Solomon Feferman. Gödel’s functional ("Dialectica") interpretation. In S. Buss, editor, Handbook of proof theory, volume 137 of Studies in logic and the foundations of mathematics, pages 337-405. North Holland, Amsterdam, 1998. Google Scholar
  2. Michael Barr. *-autonomous categories and linear logic. Mathematical structures in computer science, 1(2):159-178, 1991. Google Scholar
  3. Andrej Bauer. The Dialectica interpretation in Coq. Available electronically at http://math.andrej.com/2011/01/03/the-dialectica-interpertation-in-coq/, 2011. Google Scholar
  4. P. N. Benton. A mixed linear and non-linear logic: proofs, terms and models (preliminary report). Technical report, University of Cambridge, 1994. Google Scholar
  5. Bodil Biering. Cartesian closed Dialectica categories. Annals of pure and applied logic, 156(2-3):290-307, 2008. Google Scholar
  6. Andreas Blass. A game semantics for linear logic. Annals of pure and applied logic, 1991. Google Scholar
  7. Valeria de Paiva. The dialectica categories. In Proc. of categories in computer science, 1989. Google Scholar
  8. Valeria de Paiva. Categorical multirelations, linear logic and petri nets. Technical report, University of Cambridge, 1991. Google Scholar
  9. Valeria de Paiva. The dialectica categories. Technical report, University of Cambridge, 1991. Google Scholar
  10. Valeria de Paiva. Lineales: algebras and categories in the semantics of linear logic. In D. Barker-Plummer, D. Beaver, Johan van Benthem, and P. Scotto di Luzio, editors, Words, Proofs and Diagrams. CSLI, 2002. Google Scholar
  11. Valeria de Paiva. Dialectica and Chu construtions: Cousins? Theory and applications of categories, 17(7):127-152, 2007. Google Scholar
  12. Pieter Hofstra. The dialectica monad and its cousins. In Models, Logics, and Higher-dimensional Categories: A Tribute to the Work of Mihaly Makkai, volume 53 of CRM Proceedings and Lecture Notes, pages 107-139. American Mathematical Society, 2011. Google Scholar
  13. Martin Hyland. Proof theory in the abstract. Annals of pure and applied logic, 114(1-3):43-78, 2002. Google Scholar
  14. Martin Hyland. Slides of an invited lecture `Fibrations in Logic' at Category Theory 2007, Coimbra, Portrugal. Available electronically at https://www.dpmms.cam.ac.uk/ martin/Research/Slides/ct2007.pdf, 2007. Google Scholar
  15. Martin Hyland and Luke Ong. Fair games and full completeness for multiplicative linear logic without the MIX rule. Unpublished manuscript, 1993. Google Scholar
  16. Martin Hyland and Andrea Schalk. Glueing and orthogonality for models of linear logic. Theoretical computer science, 294(1-2):183-231, 2003. Google Scholar
  17. Ulrich Kohlenbach. Applied proof theory: proof interpretations and their use in mathematics. Springer, 2008. Google Scholar
  18. Saunders Mac Lane. Categories for the working mathematician. Springer, 1978. Google Scholar
  19. 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
  20. Paul-André Melliès. Asynchronous games 3: An innocent model of linear logic. Proceedings of the 10th Conference on Category Theory and Computer Science, 2004. Google Scholar
  21. Paul-André Melliès. Asynchronous games 4: A fully complete model of propositional linear logic. Proceedings of the 20th Conference on Logic in Computer Science, 2005. Google Scholar
  22. Paul-André Melliès. Categorical semantics of linear logic. In Interactive models of computation and program behaviour. Société Mathématique de France, 2009. Google Scholar
  23. Alexandre Miquel. A model for impredicative type systems with universes, intersection types and subtyping. In In Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS'00), 2000. Google Scholar
  24. Paulo Oliva. Computational interpretations of classical linear logic. Proceedings of WoLLIC'07, 4576:285-296, 2007. Google Scholar
  25. Paulo Oliva. An analysis of Gödel’s dialectica interpretation via linear logic. Dialectica, 62:269-290, 2008. Google Scholar
  26. Paulo Oliva. Functional interpretations of linear and intuitionistic logic. Information and Computation, 208(5):565-577, 2010. Google Scholar
  27. Philip J. Scott. The "Dialectica" interpretation and categories. Mathematical logic quarterly, 24(31-36):553-575, 1978. Google Scholar
  28. Masaru Shirahata. The dialectica interpretation of first-order classical affine logic. Theory and applications of categories, 2006. Google Scholar
  29. Matthijs Vákár. Syntax and semantics of linear dependent types. Technical report, University of Oxford, 2014. Google Scholar
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact