Categorical Models for Simply Typed Resource Calculi
Monday 12 April 2010 at 03.30 PM by damiano
Séminaire LCR : Giulio Manzonetto
Monday 12 April 2010 at 03.30 PM
Location: D214, LIPN — Duration: one hour
Le 12 avril 2010, à 15h30 en salle D214 (attention à la salle inhabituelle !), le séminaire LCR accueille Giulio Manzonetto (LIPN).
In this talk we will present two resource sensitive lambda-calculi. The first one is the resource calculus, a non-lazy version of Boudol’s lambda calculus with multiplicities.
In this calculus there are two kinds of resources: intuitionistic ones that can be erased and copied, and linear ones that must be used exactly once.
The second calculus is Ehrhard and Reignier’s differential lambda calculus. In this calculus there are two kinds of applications: the usual application of lambda calculus and a linear application. This last one is useful to define a syntactical derivative operator on terms. We will see that these two calculi are strongly linked and that - in particular - the resource calculus can be easily translated into the differential one.
Subsequently, we will provide sufficient conditions on Blute-Cockett-Seely’s Cartesian differential categories for being categorical models of the differential lambda calculus (and of the resource calculus by translation).
Finally, we will see that the concrete categories previously introduced as models of these calculi are instances of this abstract definition.