Dialectica Categories and Games with Bidding
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.
Linear logic
Dialectica categories
categorical semantics
model theory
game semantics
dependent types
functional interpretations
89-110
Regular Paper
Jules
Hedges
Jules Hedges
10.4230/LIPIcs.TYPES.2014.89
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.
Michael Barr. *-autonomous categories and linear logic. Mathematical structures in computer science, 1(2):159-178, 1991.
Andrej Bauer. The Dialectica interpretation in Coq. Available electronically at http://math.andrej.com/2011/01/03/the-dialectica-interpertation-in-coq/, 2011.
P. N. Benton. A mixed linear and non-linear logic: proofs, terms and models (preliminary report). Technical report, University of Cambridge, 1994.
Bodil Biering. Cartesian closed Dialectica categories. Annals of pure and applied logic, 156(2-3):290-307, 2008.
Andreas Blass. A game semantics for linear logic. Annals of pure and applied logic, 1991.
Valeria de Paiva. The dialectica categories. In Proc. of categories in computer science, 1989.
Valeria de Paiva. Categorical multirelations, linear logic and petri nets. Technical report, University of Cambridge, 1991.
Valeria de Paiva. The dialectica categories. Technical report, University of Cambridge, 1991.
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.
Valeria de Paiva. Dialectica and Chu construtions: Cousins? Theory and applications of categories, 17(7):127-152, 2007.
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.
Martin Hyland. Proof theory in the abstract. Annals of pure and applied logic, 114(1-3):43-78, 2002.
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.
Martin Hyland and Luke Ong. Fair games and full completeness for multiplicative linear logic without the MIX rule. Unpublished manuscript, 1993.
Martin Hyland and Andrea Schalk. Glueing and orthogonality for models of linear logic. Theoretical computer science, 294(1-2):183-231, 2003.
Ulrich Kohlenbach. Applied proof theory: proof interpretations and their use in mathematics. Springer, 2008.
Saunders Mac Lane. Categories for the working mathematician. Springer, 1978.
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.
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.
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.
Paul-André Melliès. Categorical semantics of linear logic. In Interactive models of computation and program behaviour. Société Mathématique de France, 2009.
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.
Paulo Oliva. Computational interpretations of classical linear logic. Proceedings of WoLLIC'07, 4576:285-296, 2007.
Paulo Oliva. An analysis of Gödel’s dialectica interpretation via linear logic. Dialectica, 62:269-290, 2008.
Paulo Oliva. Functional interpretations of linear and intuitionistic logic. Information and Computation, 208(5):565-577, 2010.
Philip J. Scott. The "Dialectica" interpretation and categories. Mathematical logic quarterly, 24(31-36):553-575, 1978.
Masaru Shirahata. The dialectica interpretation of first-order classical affine logic. Theory and applications of categories, 2006.
Matthijs Vákár. Syntax and semantics of linear dependent types. Technical report, University of Oxford, 2014.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode