Cofree coalgebras and differential linear logic

TL;DR

This paper demonstrates that the semantics of intuitionistic linear logic in vector spaces, based on cofree coalgebras, also models differential linear logic and the simply-typed differential lambda calculus.

Contribution

It establishes that the cofree coalgebra-based vector space semantics can serve as a model for both differential linear logic and the differential lambda calculus, extending previous understanding.

Findings

Cofree coalgebras provide a valid semantics for differential linear logic.

The category of cofree coalgebras is Cartesian closed.

The model supports the simply-typed differential lambda calculus.

Abstract

We prove that the semantics of intuitionistic linear logic in vector spaces which uses cofree coalgebras is also a model of differential linear logic, and that the Cartesian closed category of cofree coalgebras is a model of the simply-typed differential lambda calculus.