In this talk, we introduce the syntax and semantics of Differential Linear Logic. We explain how its rules relate to Linear Logic's rules, and give informal intuitions in terms of functions and distributions. We show how its cut-elimination rules are a reflection of basic calculus rules. We also review Differential Lambda-calculus, with matching intuitions. At the end of the talk, we briefly review two recent development about Differential Linear Logic, in terms of Laplace transformation and co-promotion.[-]

Many models of (differential) linear logic and lambda-calculus can be regarded as a quantitative enrichment of the relational semantics of linear logic. This talk presents an introduction to these models, taking a simple but flexible approach. Relations can be enriched with coefficients drawn from any complete semiring — a structure which allows multiplication and infinite summation of quantities — and in each case we obtain a soundness result with respect to a quantitative operational semantics for a functional language with recursion, nondeterminism and quantitative effects. Examples include models that track the number of possible reduction paths, the length of the shortest reduction path, or the probability of termination of a program.[-]