Logique linéaire et paradigmes logiques du calcul
Course 2-1 offered within MPRI.
discription of this course is available in French.
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.
- 17 Jan 2017, Lecture 1: Chapters 1, 2, 3, 4
- 24 Jan 2017, Lecture 2: Chapter 5
- 31 Jan 2017, Lecture 3: Parts of Chapters 7 and 8
- 21 Feb 2017, Lecture 4: Finish Chapters 7 and 8. Part of Chapter 9.
- 28 Feb 2017: Final exam.
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.
- 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.
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.
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
Logic, Higher-order, by Dale Miller.
A short article for the
Encyclopedia of Artificial Intelligence: Second Edition,
edited by S. Shapiro, 1992.
with Higher-Order Logic by Dale Miller and
published by Cambridge University Press in June 2012 (available
This book covers the design and applications of
the λProlog programming language.