Logic in Computer Science (LICS 1995)

Paper: Games Semantics for Full Propositional Linear Logic (at LICS 1995)

Authors: François Lamarche

Abstract

We present a model of propositional Classical Linear Logic (all the connective except for the additive constants) where the formulas are seen as two-person games in which connectives are used as tokens, while the proofs are interpreted as strategies for one player. We discuss the intimate connection between these games and the structure of proofs, and prove a full completeness theorem. The main technical innovation is a ``double negation'' interpretation of CLL into Intuitionistic Linear Logic.

BibTeX

  @InProceedings{Lamarche-GamesSemanticsforFu,
    author = 	 {François Lamarche},
    title = 	 {Games Semantics for Full Propositional Linear Logic},
    booktitle =  {Proceedings of the Tenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1995},
    year =	 1995,
    editor =	 {Dexter Kozen},
    month =	 {June}, 
    pages =      {464-473},
    location =   {San Diego, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }