Games and Full Completeness for Multiplicative Linear Logic
Abramsky, Samson ; Jagadeesan, Radha
J. Symbolic Logic, Tome 59 (1994) no. 1, p. 543-574 / Harvested from Project Euclid
We present a game semantics for Linear Logic, in which formulas denote games and proofs denote winning strategies. We show that our semantics yields a categorical model of Linear Logic and prove full completeness for Multiplicative Linear Logic with the MIX rule: every winning strategy is the denotation of a unique cut-free proof net. A key role is played by the notion of history-free strategy; strong connections are made between history-free strategies and the Geometry of Interaction. Our semantics incorporates a natural notion of polarity, leading to a refined treatment of the additives. We make comparisons with related work by Joyal, Blass, et al.
Publié le : 1994-06-14
Classification: 
@article{1183744497,
     author = {Abramsky, Samson and Jagadeesan, Radha},
     title = {Games and Full Completeness for Multiplicative Linear Logic},
     journal = {J. Symbolic Logic},
     volume = {59},
     number = {1},
     year = {1994},
     pages = { 543-574},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183744497}
}
Abramsky, Samson; Jagadeesan, Radha. Games and Full Completeness for Multiplicative Linear Logic. J. Symbolic Logic, Tome 59 (1994) no. 1, pp.  543-574. http://gdmltest.u-ga.fr/item/1183744497/