An introduction to Differential Linear Logic: proof-nets, models and antiderivatives

TL;DR

This paper introduces Differential Linear Logic, providing proof-net syntax, categorical models, and conditions for antiderivatives, with specific models including sets, relations, and finiteness spaces.

Contribution

It offers the first proof-net syntax and categorical axiomatization for Differential Linear Logic, along with conditions for antiderivatives and detailed models.

Findings

Proof-net syntax for Differential Linear Logic

Categorical conditions for antiderivatives

Models based on sets, relations, and finiteness spaces

Abstract

Differential Linear Logic enriches Linear Logic with additional logical rules for the exponential connectives, dual to the usual rules of dereliction, weakening and contraction. We present a proof-net syntax for Differential Linear Logic and a categorical axiomatization of its denotational models. We also introduce a simple categorical condition on these models under which a general antiderivative operation becomes available. Last we briefly describe the model of sets and relations and give a more detailed account of the model of finiteness spaces and linear and continuous functions.