This talk is an introduction to a sheaf-based approach to programming language semantics, developed since 2011 with Clovis Eberhart, Damien Pous and Thomas Seiller.

In a sense, the intersection of presheaf models and innocent game semantics is boolean presheaves on traces with the prefix ordering. In the same sense, our approach takes the union. It proceeds in two main layers.

The high-level layer essentially implements the idea that if one considers a rich enough notion of play, then the innocence of game semantics may be encoded as a sheaf condition. Richness here means sufficient sensitivity to causality information. The sheaf condition means that any play is covered by its views, for the topology-like sense of `covered' provided by Grothendieck topologies. We will sketch our general notion of playground and how each playground gives rise to a family of categories of innocent strategies.

The low-level layer is concerned with the construction of relevant playgrounds. In the first installments of our approach, we constructed playgrounds for CCS and the pi-calculus, by hand. In recent work with Clovis, we started to generalise the process. I will illustrate this by constructing a candidate playground for the original HO games, which will turn out to also illustrate an important limitation of the current approach.