Linear logic arose from an analysis of models of the typed lambda-calculus, where function

spaces (corresponding to logical implication) decompose naturally into a modality called “of course” and another implication called linear implication. These two connectives are echoing the difference between terms and linear terms, which are terms in which each variable occurs exactly once. As for the modality, it expresses the ability for a function to use its argument more than once during the computation. This seminal observation led to a ressource-avare logic, combining the beautiful dualities of classical logic with the constructive features of intuitionistic logic. I will cover the syntactic aspects: sequent calculus, proof nets, cut-elimination. I shall introduce enough category theory to explain the models of linear logic. Much in the same way as linear logic arose from models of the lambda-calculus, Thomas Ehrhard found inspiration from models of linear logic to develop differential lambda-calculus and differential linear logic, establishing striking links between differentiation in the sense of mathematical analysis and the fine analysis of substitution in the syntax. Explaining Ehrhard’s ideas will occupy the second part of the lecture series.

Idioma: Inglés.

Requisitos: Conocimiento general de lenguajes de programación.