In the first part of this talk, I'll recall the construction of category of games and innocent deterministic strategies introduced by Harmer, Hyland and Mellies [1]. Compared with the original method by Hyland and Ong [2], this method holds two specific advantages. First, it outlines the structural conditions on certain games and strategies by introducing separate entities (the schedules) that focus most of the required proof work. Second, the methods lays out a pretty clear combinatorial ‘recipe’ that could be replicated in other settings. That will be the goal of the second part of the talk, which will develop a 2-categorical and sheaf-theoretic formulation of non-deterministic innocent strategies, based on this ‘recipe’. During the course of this construction, I'll outline specific properties that give us a better understanding of both deterministic and non-deterministic strategies.
[1] Categorical combinatorics of innocent strategies, Harmer, Hyland, Mellies, LiCS 2007.
[2] On full abstraction for PCF I, II and III, Hyland, Ong, Information and Computation 2000.