Paper: Asynchronous Games 4: A Fully Complete Model of Propositional Linear Logic (at LICS 2005)

Authors: Paul-André Melliès

Abstract

We construct a denotational model of propositional linear logic based on asynchronous games and winning uniform innocent strategies. Every formula A is interpreted as an asynchronous game [A] and every proof ? of A is interpreted as a winning uniform innocent strategy [?] of the game [A]. We show that the resulting model is fully complete: every winning uniform innocent strategy ? of the asynchronous game [A] is the denotation [?] of a proof ð of the formula A.

BibTeX

  @InProceedings{Mellis-AsynchronousGames4A,
    author = 	 {Paul-André Melliès},
    title = 	 {Asynchronous Games 4: A Fully Complete Model of Propositional Linear Logic},
    booktitle =  {Proceedings of the Twentieth Annual IEEE Symposium on Logic in Computer Science (LICS 2005)},
    year =	 {2005},
    month =	 {June}, 
    pages =      {386--395},
    location =   {Chicago, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }