Projects per year
Abstract
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.
Original language | English |
---|---|
Pages (from-to) | 247-264 |
Number of pages | 18 |
Journal | Information and Computation |
Volume | 222 |
Early online date | 26 Oct 2012 |
DOIs | |
Publication status | Published - Jan 2013 |
Keywords
- differential categories
- game semantics
- full abstraction
Fingerprint
Dive into the research topics of 'Constructing differential categories and deconstructing categories of games'. Together they form a unique fingerprint.Projects
- 1 Finished
-
Semantic Structures for Higher-Order Information Flow
Laird, J. (PI)
Engineering and Physical Sciences Research Council
20/06/10 → 19/06/12
Project: Research council