University of Birmingham > Talks@bham > Theoretical computer science seminar > Constructing Differential Categories and Deconstructing Categories of Games

Constructing Differential Categories and Deconstructing Categories of Games

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.