Constructing Differential Categories and Deconstructing Categories of Games

Add to your list(s) Download to your calendar using vCal

• Guy McCusker, University of Bath
• Friday 13 January 2012, 16:00-17:00
• UG40 Computer Science.

If you have a question about this talk, please contact Paul Levy.

We present an abstract construction of models of intuitionistic linear logic which are also differential categories in the sense of Blute, Cockett and Seely. The Kleisli categories for the associated exponential comonads are Cartesian-closed and provide models of typed versions of Ehrhard’s Differential Lambda-Calculus, or equally, typed Resource Calculi as presented by Pagani and Tranquilli. Applying the construction to the terminal category gives the category MRel of “multiset relations”, which is the leading example of a model of differential lambda-calculus. Applying the construction to a category of games, we recover a games model previously used to interpret nondeterministic imperative programs, and hence discover differential structure in that model. Refining the games model with a notion of causal independence yields a model of “Resource PCF ” with the finite definability property. Comparison of this model with MRel reveals that MRel also has this property, and hence the model of Resource PCF in MRel is fully abstract.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Theoretical computer science seminar
• UG40 Computer Science
• computer sience

Note that ex-directory lists are not shown.