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.
Trasfondo sobre teoría de prueba y Curry-Howard. Lógica lineal (sintaxis y modelos). Redes de prueba. Lógica lineal diferencial, y otras extensiones y variaciones.
Conocimiento general de lenguajes de programación.
P.-L. Curien, Introduction to linear logic and ludics, part I, Advances in Mathematics (China) 34 (5), 513-544 (2005), and part II, Advances in Mathematics (China) 35 (1),
1-44 (2006) (available here: https://www.irif.fr/~curien/LL-ludintroI.pdf.
T. Ehrhard, An introduction to differential linear logic: proof-nets, models and an- tiderivatives, Mathematical Structures in Computer Science 28(7), 995-1060 (2018).
J.-Y. Girard, Linear logic, Theoretical Computer Science 50, 1-102 (1987). Handbook of linear logic, collective book in development, regularly updated at https: //ll-handbook.frama.io/ll-handbook/ll-handbook-public.pdf.