Differential categories were introduced by Blute, Cockett and Seely to axiomatize categorically Ehrhard and Regnierʼs syntactic differential operator. We present an abstract construction that takes a symmetric monoidal category and yields a differential category, and show how this construction may be applied to categories of games. In one instance, we recover the category previously used to give a fully abstract model of a nondeterministic imperative language. The construction exposes the differential structure already present in this model, and shows how the differential combinator may be encoded in the imperative language. A second instance corresponds to a new cartesian differential category of games. We give a model of a simply-typed resource calculus, Resource PCF, in this category and show that it possesses the finite definability property. Comparison with a semantics based on Bucciarelli, Ehrhard and Manzonettoʼs relational model reveals that the latter also possesses this property and is fully abstract.
- differential categories
- game semantics
- full abstraction
Laird, J., Manzonetto, G., & McCusker, G. (2013). Constructing differential categories and deconstructing categories of games. Information and Computation, 222, 247-264. https://doi.org/10.1016/j.ic.2012.10.015