Logique linéaire et paradigmes logiques du calcul
Course 2-1 offered within MPRI.
discription of this course is available in French.
Delia Kesner, and
During 2021-2022, Miller's lectures will be on Wednesday from 16h15 - 19h15.
Lectures will be in room 1002 in Bâtiment Sophie Germain.
Miller will lecture (in English) on the following five dates:
22, 29 September, 6, 13, 20 October.
Miller will be lecturing from the monograph
Proof theory, proof search, and logic programming.
- The current draft is dated 20 October
- Comments, corrections, criticism of this draft are welcome.
Many of the exercises discussed in class and used on the final exam
are taken from this text. This monograph is being actively revised
so look for corrected or extended versions of these notes as the
semester progresses. Comments and corrections are welcome.
- 22 Sep 2021, Lecture 1: The basics of sequent calculus. Chapters
1, 2, and 3 from Miller's lecture notes.
- 29 Sep 2021, Lecture 2: Sequent calculus for classical and
intuitionistic logics. Chapter 4 and the start of Chapter 5..
- 6 Oct 2021, Lecture 3: Goal-directed search, focused proofs in
intuitionistic logic, and logic programming examples. Chapter
5. (Material on Kripke models in Section 5.6 will not be covered.)
- 13 Oct 2021, Lecture 4: Chapter 6 up to but not including Section 6.4.
- 20 Oct 2021, Lecture 5: Present Section 6.5 and Chapter 7. Some
examples will also be taken from Chapter 9 and from
The date and modality of this exam will be determined later.
References and Links
Below are some documents available via the web that may be of use
in this class.
- Introduction to Linear Logic by
Roberto Di Cosmo and Vincent Danos will be referenced for some lectures.
- Linear Logic,
by Roberto Di Cosmo and Dale Miller, The Stanford Encyclopedia of
Philosophy (Winter 2016 Edition), Edward N. Zalta (ed.).
- 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.