Logic in Computer Science (LICS 2005)

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

Authors: Paul-Andre Mellies

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{Mellies-AsynchronousGames4A,
    author = 	 {Paul-Andre Mellies},
    title = 	 {Asynchronous Games 4: A Fully Complete Model of Propositional Linear Logic},
    booktitle =  {Proceedings of the Twentieth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2005},
    year =	 2005,
    editor =	 {Prakash Panangaden},
    month =	 {June}, 
    pages =      {386--395},
    location =   {Chicago, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }