Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Thirteenth Annual IEEE Symposium on

Logic in Computer Science (LICS 1998)

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 Gi with optimised strategies; we show that the denotational semantics in Gi 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}
  }
   

Last modified: 2018-06-2121:59
Andrzej Murawski