Internship report: Coherent differentiation in models of Linear Logic

TL;DR

This paper demonstrates that coherent differentiation extends differential categories by showing that the deriving transformation in a differential category with a categorical product induces coherent differentiation, broadening the theoretical framework for models of computation.

Contribution

It proves that the deriving transformation in differential categories with categorical products induces coherent differentiation, establishing it as a genuine generalization.

Findings

Deriving transformation induces coherent differentiation in differential categories.

Coherent differentiation generalizes differential categories.

Supports models of computation with partial sums.

Abstract

Coherent differentiation was introduced by Ehrhard in order to generalize differential categories to a setting in which the sum is only partially defined, in order to account for the deterministic nature of most models of computation. This internship report proves that the deriving transformation of a differential category with a categorical product always induces a coherent differentiation. This ensures that coherent differentiation is indeed a generalization of differential categories.