Roberto Di Cosmo: Linear Logic Course Notes

The Linear Logic Primer

This is an ever evolving support, elaborated together with one of the very experts of Linear Logic, Vincent Danos, for an introductory course on Linear Logic that has been taught on several occasions in different continents over the past years.

The original Pisa Version (1992)

This is a short rugged presentation of the material, but already has a fan club, so we still keep it here (dvi).

The current major revision

This is the support being used since 1996/1997 in a course in the Dea de Sémantique, Preuves et Programmation.

Course Notes (.pdf)

Selected exam texts

Examen 1999/2000

General surveys

An introductory survey article co-written with Dale Miller for the Stanford Encyclopedia of Phylosophy is available online since September 2006.

Some useful web pointers: (no claim to give a complete list implied)

Articles of the founding father Jean-Yves Girard
Some papers relating Linear Logic to Explicit Substitutions and Type Isomorphisms
- A linear logical view of Linear Type Isomorphisms, Vincent Balat, Roberto Di Cosmo CSL 1999
- Strong normalization of Proof Nets modulo Structural Congruences, Roberto Di Cosmo, Stefano Guerrini RTA 1999
- Proof Nets and Explicit Substitutions, Roberto Di Cosmo, Delia Kesner, Emmanuel Polonowski MSCS 2002
Some papers relating with modal logics
- Proof nets, Garbage, and Computations, S. Guerrini, S.Martini and A. Masini, Theoretical Computer Science, vol. 253, n. 2, pp. 185-237, 2001
- Parsing MELL Proof Nets, S. Guerrini and A. Masini, Theoretical Computer Science, vol. 254, n. 1-2, pp. 317 - 335, 2001
- Modal Logic, Linear Logic, Optimal Lambda-reduction , S. Guerrini, S.Martini and A. Masini in Logic and Foundations of Mathematics, A. Cantini, E. Casari, P. Minari eds., Kluwer, Dordrecht, 1999.
- An analysis of (linear) exponentials based on extended sequents . S. Guerrini, S. Martini and A. MasiniLogic Journal of IGPL, 6:735-753,1998
Optimal reduction through Linear Logic: The BOHM experiment (source code) in Andrea Asperti's public ftp directory
A survey and bibliography of Linear Logic Programming
An extensive online bibliography

Local Pointers

PPS Roberto Di Cosmo

Roberto Di Cosmo