From differential linear logic to coherent differentiation

Abstract In thise survey, we present in a unified way the categorical and syntactical settings of coherent differentiation introduced recently, which shows that the basic ideas of differential linear logic and of the differential lambda-calculus are compatible with determinism. Indeed, due to the Leibniz rule of the differential calculus, differential linear logic and the differential lambda-calculus feature an operation of addition of proofs or terms operationally interpreted as a strong form of nondeterminism. The main idea of coherent differentiation is that the summations required by differentiation can be controlled and kept deterministic, in the denotational models, as well as in the syntax and operational semantics themselves. In sharp contrast with the differential lambda-calculus, coherent differentiation indeed allows one to design differential extensions of Turing complete functional programming languages, such as PCF, endowed with a deterministic evaluation mechanism, typically implemented in a Krivine abstract machine.