Paper Info
Title
An Indexed System for Multiplicative Additive Polarized Linear Logic
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 Iwork 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 MALLPby establishing a correspondence between the provability of indexed formulas and relations that can be extended to (non-indexed) proof-denotations.
Year
DOI
Venue
2008
10.1007/978-3-540-87531-4_20
CSL
Keywords
Field
DocType
indexed system,denotational semantics,logical system,linear logic,web-based instance,denotational construction,multiplicative additive,multiplicative additive linear logic,multiplicative additive polarized linear,sf mallp,adjoint pair,denotational model,indexation
Discrete mathematics,Multiplicative function,Denotational semantics,Linear logic,Mathematics
Conference
Volume
ISSN
Citations 
5213
0302-9743
3
PageRank 
References 
Authors
0.44
9
2
Name
Order
Citations
PageRank
Masahiro Hamano1397.66
Ryo Takemura2859.52