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 -