Logique linéaire et paradigmes logiques du calcul

Course 2-1 offered within MPRI.

A brief discription of this course is available in French.

Instructors

Instructors: Roberto DiCosmo, Delia Kesner, Dale Miller, and Stéphane Lengrand.

Venue

Miller speaks on the following dates (Mondays) from 13h15 to 15h45.

• 10 Dec 2012: CANCELLED. Class will be made up.
• 17 Dec 2012: Lecture 1. (1E01 Chevaleret)
• 7 Jan 2013: Lecture 2. (Batiment Sophie Germain room 1009) Chapter 4 plus Chapter 5 up to (and including) 5.3.
• 14 Jan 2013: Lecture 3. (Batiment Sophie Germain room 1009)
• 21 Jan 2013: Lecture 4. (Batiment Sophie Germain room 1009)
• 4 Feb 2013: Lecture 5. (Batiment Sophie Germain room 1009) Topic: the LJF and LKF focused proof systems for intuitionistic and classical logics.

Exam

An example exam for Miller's part of the class: pdf.

References and Links

The lecture notes for most of the first four lectures is available in pdf format.

Below are some documents available via the web that may be of use in this class.

1. Logic for Computer Science: Foundations of Automatic Theorem Proving, by Jean Gallier, Wiley, pp. 511 (1986). This book is now out of print but available for free download.
2. Proofs and Types by Jean-Yves Girard, Paul Taylor, and Yves Lafont. Cambridge University Press. This book is now available from a number of sources for free download. Try the link above to find locations for downloading. Also available here.
3. Proof Theory as an Alternative to Model Theory by Dale Miller. Argues that the theory of proofs should also be considered a foundations for the design and justification of logic programming.
4. Logic, Higher-order, by Dale Miller. A short article for the Encyclopedia of Artificial Intelligence: Second Edition, edited by S. Shapiro, 1992. (DVI, PDF).