Recursive types in games: axiomatics and process representation

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