In this work in progress, we show that the Taylor expansion of a λ-term is isomorphic to its interpretation in pointer concurrent games.

Tsukada and Ong showed in 2016 that (β-normal, η-long) resource terms correspond to plays of Hyland-Ong games (up to Mellies’ homotopy equivalence). These results were recently extended by the authors using pointer concurrent games, a game model inspired from concurrent games which represents plays quotiented by homotopy. Normal, η-long resource terms are isomorphic to augmentations (canonical representatives of Hyland-Ong plays up to homotopy), and that isomorphism is compatible with the β-reduction.

Taylor expansion translates a λ-term (with possibly infinite behavior) to an infinite sum of resource λ-terms. We define a Taylor expansion sending simply-typed λ-terms to terms of the simply-typed, η-long resource calculus, and we extend the previous isomorphism to show that game semantics is compatible with Taylor expansion.