Categorical Models for Simply Typed Resource Calculi

We introduce the notion of differential λ-category as an extension of Blute-Cockett-Seely's differential Cartesian categories. We prove that differential λ-categories can be used to model the simply typed versions of: (i) the differential λ-calculus, a λ-calculus extended with a syntactic derivative operator; (ii) the resource calculus, a non-lazy axiomatisation of Boudol's λ-calculus with multiplicities. Finally, we provide two concrete examples of differential λ-categories, namely, the category MRel of sets and relations, and the category MFin of finiteness spaces and finitary relations.