The substantial piece of work described here culminates in a denotational semantic definition of the fixed point calculus (FPC), seen as a sequential functional programming language. As such, this paper extends the seminal work of Plotkin on PCF (a programming language for computable functions). PCF has recursively defined functions, whereas FPC also has recursively defined types.

The categorical model is shown to be both sound and complete (that is, fully abstract) and, hence, to capture exactly the behavior of programs in FPC. It is built on the notion of a game between a player (the system) and an opponent (the environment). They take turns, just as in a traditional two-person game. Long, tedious, but well-described and well-motivated constructions lead us through notions of valid positions, the playing of games, (deterministic) strategies, innocent strategies, and well-opened games (in which valid initial moves can never be repeated).

The author then discusses categories, in which games are objects and innocent strategies are morphisms. He progressively develops the construction to achieve a Cartesian closed category of sequential functions and includes sums that can be used to model choices from different strategies.

The FPC language is then introduced and formally defined. Its semantics is defined in terms of morphisms (in the resultant category) that model exactly the strategies of the FPC program under consideration.

Finally, the author shows that all finite strategies between finite types are definable.

The paper, submitted in 1996 (as a contribution to a special issue based on the 1996 LICS conference), necessarily contains extended and reworked material done in collaboration with others. It is a long but worthwhile read.