Logique linéaire et paradigmes logiques du calcul
Course 2-1 offered within MPRI.
discription of this course is available in French.
Beniamino Accattoli, and
During 2023-2024, Miller's lectures will be on Tuesdays from 16h15 - 19h15.
Miller will lecture (in English) on the following four dates:
12, 19, 26 September, 3 October.
Lectures will be in room 1002 in Bâtiment Sophie
Germain, except for the first class (12 Sep) which
will be in building Halle aux Farines room 381F.
Miller will be lecturing from his monograph
Proof theory, proof search, and logic programming.
- The current draft is dated 11
September 2023. This is the version that will be used during my
- Comments, corrections, and criticism on this draft are welcome.
Many of the exercises discussed in class and used on the final exam
are taken from this text.
- 12 Sep 2022, Lecture 1: Preface and Chapters 1-3 of lecture notes.
- 19 Sep 2022, Lecture 2: Chapter 4 and the start of Chapter 5.
- 26 Sep 2022, Lecture 3: Complete Chapter 5, excluding 5.5 and
5.6. Start Chapter 6.
- 3 Oct 2022, Lecture 4:
- Midterm exam: 21 Nov 2023.
A sample example is available.
The following sections are not covered by the exam: Sections 5.5, 5.6,
6.7, and 6.8. Also not covered: Sections 7.5 to the end of the book.
The exam for my lectures will be held joint with Prof Kesner's
lectures. These exams will be held on 21 November 2023
during the same hour and lecture room as the other classes.
References and Links
Below are some documents available via the web that may be of use
in this class.
- Linear Logic,
by Roberto Di Cosmo and Dale Miller, The Stanford Encyclopedia of
Philosophy (Winter 2016 Edition), Edward N. Zalta (ed.).
- Introduction to Linear Logic by
Roberto Di Cosmo and Vincent Danos will be referenced for some lectures.
- A Survey of the Proof-Theoretic Foundations of Logic
Programming by Dale Miller.
To appear in the
Anniversary Issue of the
Theory and Practice of Logic Programming (TPLP). Published online November 2021.
- 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 foundation 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.