Logique linéaire et paradigmes logiques du calcul

Course 2-1 offered within MPRI.

A brief discription of this course is available in French and English.

Instructors

Instructors: Roberto DiCosmo, Delia Kesner, Stefano Guerrini, and Dale Miller.

Venue

Miller speaks on 8, 15, 22, 29 Jan (Fridays) from 13h to 16h in 8B01 Chevaleret. The ``partiel'' will be held on either 5 or 12 February.

• 8 Jan 2010: Covered material up to and including Exercise 8, page 21.
• 15 Jan 2010:
• 22 Jan 2010:
• 29 Jan 2010:
• New: 12 Feb 2010, 1C18, all documents are allowed.

Exam

An example exam for Miller's part of the class: pdf. To find one for Guerrini's part of the class, see his web page.

References and Links

Lecture notes will be handed out at the first lecture. They are also available in pdf format (draft dated January 2010.)

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).