Semantics Club 04 05 2001
I will give some more detail on the theoretical story behind my recent Lab Lunch talk. In particular, I will define more precisely the category of types and strategies I have in mind. I arrived at this category simply as the Karoubi envelope of a certain lambda algebra, but it turns out to be essentially the same as Abramsky's category of games and strategies with no innocence or well-bracketing constraints. I will also consider the expressive power of the corresponding programming languages, and the implications of this model for programming language semantics and logic.
I will also sketch some ideas not mentioned at Lab Lunch: the use of this category for modelling objects with persistent internal state (as in object-oriented languages). It appears that the CCC of strategies is equipped with a natural "state monad", giving rise to an SMC category of algebras which seems to be suitable for modelling object-oriented styles of computation.
All this stuff is work in progress and as yet poorly understood.