Paper: Recursive Types in Games: Axiomatics and Process Representation (at LICS 1998)

Authors: Marcelo P. Fiore Kohei Honda

Abstract

This paper presents two basic results on game-based semantics of FPC, a metalanguage with sums, products, exponentials and recursive types. First we give an axiomatic account of the category of games G, offering a fundamental structural analysis of the category as well as a transparent way to prove computational adequacy. As a consequence we obtain an intensional full-abstraction result through a standard definability argument. Next we extend the category G by introducing a category of games G_i with optimised strategies; we show that the denotational semantics in G_i gives a compilation of FPC terms into core Pict codes (the asynchronous polyadic π-calculus without summation). The process representation follows a pioneering idea of Hyland and Ong (1995). However we advance their representation by introducing semantically well-founded optimisation techniques; we also extend the setting to encompass the rich type structure of FPC. The resulting code gives basic insight on the relationship between the abstract, categorical, types and their possible implementations

BibTeX

  @InProceedings{FioreHonda-RecursiveTypesinGam,
    author = 	 {Marcelo P. Fiore and Kohei Honda},
    title = 	 {Recursive Types in Games: Axiomatics and Process Representation},
    booktitle =  {Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1998)},
    year =	 {1998},
    month =	 {June}, 
    pages =      {345--356},
    location =   {Indianapolis, IN, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }