TY - GEN

T1 - An indexed system for multiplicative additive polarized linear logic

AU - Hamano, Masahiro

AU - Takemura, Ryo

PY - 2008

Y1 - 2008

N2 - 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 describe (in a proof-theoretical manner) the denotational construction of the corresponding rules of MALLP. We show that 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.

AB - 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 describe (in a proof-theoretical manner) the denotational construction of the corresponding rules of MALLP. We show that 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.

UR - http://www.scopus.com/inward/record.url?scp=57849142937&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=57849142937&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-87531-420

DO - 10.1007/978-3-540-87531-420

M3 - Conference contribution

AN - SCOPUS:57849142937

SN - 3540875301

SN - 9783540875307

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 262

EP - 277

BT - Computer Science Logic - 22nd International Workshop, CSL 2008 - 17th Annual Conference of the EACSL, Proceedings

T2 - 22nd International Workshop on Computer Science Logic, CSL 2008, and 17th Annual Conference of the European Association for Computer Science Logic, EACSL

Y2 - 16 September 2008 through 19 September 2008

ER -