Programme

Sequent Calculus Proofs
***************************************
Natural Deduction

Sequent Calculus for Classical Logic (LK) and Intuitionistic Logic (LJ)

Cut elimination for LK and LJ sequent proofs

Sequent calculus for Linear Logic(LL)

Cut Elimination Theorem for LL

Focusing Theorem for LL proofs

Proof Nets
*************************************
(proof-structures, correctness, normalization, adequacy, sequentialization, focusing, complexity)

Pure Multiplicative Proof Nets

Multiplicative and Additive Proof Nets

Multiplicative and Exponenial Proof Nets

Core Documentation

Handbooks, papers, NOTES AND SLIDES AVAILABLE ON THE COURSE WEB PAGE
https://sites.google.com/view/lm510/

Reference Bibliography

J.-Y. Girard, Proofs and Types AA.VV., Handbook of Linear Logic V. Danos and L. Regnier, The structure of Multiplicatives O. Laurent, Sequentialization of Multiplicative Proof Nets J.-M. Andreoli and R. Maieli, Focusing and proof nets in linear and non-commutative logic R. Maieli, Cut Elimination for Monomial Proof Nets of the Purely Multiplicativeand Additive Fragment of Linear Logic D. Mazza, Attack of the Exponentials C. Retoré, On the relation between coherence semantics and multiplicative proof nets

Type of delivery of the course

LECTURES WITH EXERCISES in classroom and by streaming

Type of evaluation

questions and exercises on the topics covered in class with an individual seminar