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: Roberto DiCosmo, Delia Kesner, Stéphane Lengrand, and Dale Miller.

Lecture Notes

The lecture notes for most of the first four lectures are handed out the first day of class. They are also available here.


Miller speaks on the following Tuesdays from 16h15 to 19h15. All lectures are planned for Batiment Sophie Germain room 2035. Miller will lecture in English.


The exam for the second part of this course will be on either 28 February or 7 March 2017. To prepare for the exam, read the lecture notes and do the exercises in them.

References and Links

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).
  5. Programming with Higher-Order Logic by Dale Miller and Gopalan Nadathur, published by Cambridge University Press in June 2012 (available via Amazon). This book covers the design and applications of the λProlog programming language.