Abstract
We present an indexed logical system MALLP( I) for Laurent’s multiplicative additive polarized linear logic (MALLP) [14]. The system is a polarized variant of Bucciarelli-Ehrhard’s indexed system for multiplicative additive linear logic [4]. Our system is derived from a web-based instance of Hamano-Scott’s denotational semantics [12] for MALLP. The instance is given by an adjoint pair of right and left multi-pointed relations. In the polarized indexed system, subsets of indexes for I work as syntactical counterparts of families of points in webs. The rules of \(\sf MALLP({\it I})\) describe (in a proof-theoretical manner) the denotational construction of the corresponding rules of MALLP. We show that \(\sf MALLP({\it I})\) faithfully describes a denotational model of MALLP by establishing a correspondence between the provability of indexed formulas and relations that can be extended to (non-indexed) proof-denotations.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Andreoli, J.-M.: Logic Programming with Focusing Proofs in Linear Logic. Journal of Logic and Computation 2(3), 297–347 (1992)
Blute, R., Scott, P.J.: Category theory for linear logicians. In: Ruet, P., Ehrhard, T., Girard, J.-Y., Scott, P. (eds.) Proceedings Linear Logic Summer School, pp. 1–52. Cambridge University Press, Cambridge (2004)
Bruasse-Bac, A.: Logique linéaire indexée du second ordre, Thèse de doctorat, Institut de Mathématiques de Luminy, Université Aix-Marseille II (2001)
Bucciarelli, A., Ehrhard, T.: On phase semantics and denotational semantics in multiplicative-additive linear logic. Annals of Pure and Applied Logic 102(3), 247–282 (2000)
Bucciarelli, A., Ehrhard, T.: On phase semantics and denotational semantics: the exponentials. Annals of Pure and Applied Logic 109(3), 205–241 (2001)
Cockett, R., Seely, R.: Polarized category theory, modules, and game semantics. Theory and Applications of Categories 18(2), 4–101 (2007)
Ehrhard, T.: A completeness theorem for symmetric product phase spaces. Journal of Symbolic Logic 69(2), 340–370 (2004)
Girard, J.-Y.: A New Constructive Logic: Classical Logic. Mathematical Structures in Computer Science 1(3), 255–296 (1991)
Girard, J.-Y.: On denotational completeness. Theoretical Computer Science 227(1), 249–273 (1999) (special issue)
Girard, J.-Y.: On the meaning of logical rules II: multiplicative/additive case. In: Foundation of Secure Computation. NATO Series F, vol. 175, pp. 183–212. IOS Press, Amsterdam (2000)
Girard, J.-Y., Solum, L.: From the rules of logic to the logic of rules. Mathematical Structures in Computer Science 11(3), 301–506 (2001)
Hamano, M., Scott, P.: A Categorical Semantics for Polarized MALL. Annals of Pure and Applied logic 145, 276–313 (2007)
Hamano, M., Takemura, R.: A Phase Semantics for Polarized Linear Logic and Second Order Conservativity (submitted, 2007)
Laurent, O.: Étude de la polarisation en logique, Thèse de Doctorat, Institut de Mathématiques de Luminy, Université Aix-Marseille II (2002)
Laurent, O.: Polarized games. Annals of Pure and Applied Logic 130(1-3), 79–123 (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hamano, M., Takemura, R. (2008). An Indexed System for Multiplicative Additive Polarized Linear Logic. In: Kaminski, M., Martini, S. (eds) Computer Science Logic. CSL 2008. Lecture Notes in Computer Science, vol 5213. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-87531-4_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-87531-4_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-87530-7
Online ISBN: 978-3-540-87531-4
eBook Packages: Computer ScienceComputer Science (R0)