This special issue is devoted to some aspects of the new ideas that recently arose from the work of Thomas Ehrhard on the models of linear logic (LL) and of the λ-calculus. In some sense, the very origin of these ideas dates back to the introduction of LL in the 80s by Jean-Yves Girard. An obvious remark is that LL yielded a first logical quantitative account of the use of resources: the logical distinction between linear and non-linear formulas through the introduction of the exponential connectives. As explicitly mentioned by Girard in his first paper on the subject, the quantitative approach, to which he refers as ‘quantitative semantics,’ had a crucial influence on the birth of LL. And even though, at that time, it was given up for lack of ‘any logical justification’ (quoting the author), it contained rough versions of many concepts that were better understood, precisely introduced and developed much later, like differentiation and Taylor expansion for proofs. Around 2003, and thanks to the developments of LL and of the whole research area between logic and theoretical computer science, Ehrhard could come back to these fundamental intuitions and introduce the structure of finiteness space, allowing to reformulate this quantitative approach in a standard algebraic setting. The interpretation of LL in the category Fin of finiteness spaces and finitary relations suggested to Ehrhard and Regnier the differential extensions of LL and of the simply typed λ-calculus: Differential Linear Logic (DiLL) and the differential λ-calculus. The theory of LL proof-nets could be straightforwardly extended to DiLL, and a very natural notion of Taylor expansion of a proof-net (and of a λ-term) was introduced: an element of the Taylor expansion of the proof-net/term α is itself a (differential) proof-net/term and an approximation of α.
Proof nets and semi-star-autonomous categories
