Linear Logic is an active research topic, whose insights have been a breakthrough not only in proof theory, but also into the modern theory of programming languages. Linear Logic has promoted a dynamic, interactive view on computation, centered on how the computation is performed, rather than the input-output behavior. Another key aspect is that it takes into account the amount of resources needed to produce an output, yielding to quantitative approaches to types and semantics. These systems give information on the cost of computation, and they proved to be crucial to build quantitative frameworks, for example probabilistic and quantum computation. The theory of Linear Logic comes equipped with powerful tools to study the process of computation (cut-elimination/normalization), including an advanced graph formalism for proofs representation: Proof Nets.

Different foundational concepts in the theory of programming can be explained in terms of Linear Logic. In this course we propose to visit some of them, by using the viewpoint of linearity to explain and explore their underlying intuitions and properties.

This course will offer an introduction to the main tools and results of Linear Logic, and a glimpse into advanced topics (unifying settings for programming, quantitative types, program approximation, probabilistic programming), reflecting  current research directions which rely on the insights of Linear Logic.

Starting Date: 16 September!

1. Claudia Faggian : 16/09/25, 23/09/25, 30/09/25, 07/10/25, 14/10/25
2. Delia Kesner: 21/10/25, 04/11/25, 18/11/25, 09/12/25, 16/12/25
3. Giulio Manzonetto: 13/01/26, 20/01/26, 27/01/26, 03/02/26, 10/02/26
4. Three Invited Speakers (Giulio Guerrieri, Damiano Mazza, Benoit Valiron): 24/02/26

1. Part I (Faggian): Regular, short homework exercises
2. Part II (Kesner): 6 January, 12h45-14h45, room 0011, SG (all documents allowed; computers and mobile phones prohibited)
3. Part III (Manzonetto): Regular, short homework exercises

• First steps in Linear Logic: sequent calculus, cut elimination & proof search.
• Abstract rewriting: a framework to study the operational properties of formal systems.
• The graph syntax of LL: proof nets.
• The graph syntax of LL (cont.): MELL proof nets
• Sequentialization. The flow of computation: Geometry of Interaction.
• Calculi with Explicit Substitutions: main properties.
• From Lambda-Calculus to MELL Proof-Nets.
• Quantitative Types: foundations, properties, applications.
• Bang Calculus: a unifying language inspired from LL: Definition, properties, capturing CBN and CBV in the Bang Calculus.
• Observational equivalence: the call-by-name case and the call-by-value case Hands-on Lab: some proofs of key lemmas.
• Böhm trees and program approximation.
• Resource calculus. Syntactic properties: linear substitution, confluence, strong normalization.
• Taylor expansion as theory of program approximation. Inductive proof of approximation theorem and consequences.
• Semantic properties of resource calculus: relational semantics and its approximation theorem.
• The challenging case of call-by-value.

The course will by default be taught in French (Kesner, Manzonetto) and in English (Faggian), but all speakers will teach in English if explicitly requested. The exercises and exam topics will be in English. Students may write their exam in French and/or English.

• Claudia Faggian
• Delia Kesner
• Giulio Manzonetto

Basic notions of proof-theory and lambda calculus.

SEMPL, FUN, PRFSYS, PRFA

• J.-Y. Girard: Linear Logic. Theor. Comput. Sci. 50: 1-102 (1987)
• Handbook of Linear Logic, available online: https://ll-handbook.frama.io/ll-handbook/ll-handbook-public.pdf
• Lecture notes on Proof Nets (by O. Laurent): https://perso.ens-lyon.fr/olivier.laurent/pn.pdf
• Interactive linear logic sequent calculus prover: https://click-and-collect.linear-logic.org/ Interactive tutorial on sequent calculus: http://logitext.mit.edu/tutorial
• H. Barendregt and G. Manzonetto. A Lambda Calculus Satellite. College Publications 2022, ISBN 978-1-84890-415-6
• A. Bucciarelli and D. Kesner and D. Ventura. Non-Idempotent Intersection Types for the Lambda-Calculus. Logic Journal of the IGPL, 25(4):431--464, 2017.
• A. Bucciarelli and D. Kesner and A. Ríos and A. Viso. The Bang Calculus Revisited.Information and Computation (I&C), 293:105047, 2023.