Logique linéaire et paradigmes logiques du calcul
Course 21 offered within MPRI.
A brief
discription of this course is available in French.
Instructors
Instructors:
Dale Miller,
Delia Kesner, and
Beniamino Accattoli.
Venue
During 20202021, Miller's lectures will be on Tuesday from 16h15  19h15.
Lectures will be in room 1013 in Bâtiment Sophie Germain.
Miller will lecture (in English) on the following five dates:
15, 22, 29 September, 6, 13 October.
Lecture Notes
Two sets of lecture notes will be consulted during Miller's
lectures.
 Proof search, proof theory, and logic
programming by Miller (version 4 dated 13102020). We will
only cover Chapters 17, and 9. Many of the exercises discussed
in class and used on the final exam are taken from this document.
This monograph is being actively revised so look for corrected or
extended versions of these notes as the semester progresses.
These lecture notes are not online for the moment since they
are still being revised. If you want a copy of the current
draft, please send me mail.
 Introduction to Linear Logic by
Roberto Di Cosmo and Vincent Danos will be referenced for some lectures.
Lectures
 15 Sep 2020, Lecture 1: The basics of sequent calculus. Chapters
1, 2, and 3 from Miller's lecture notes.
 22 Sep 2020, Lecture 2: Sequent calculus for classical and
intuitionistic logics. Chapter 4.
 29 Sep 2020, Lecture 3: Goaldirected search, focused proofs in
intuitionistic logic, and Logic programming examples. Chapter
5. (Material on Kripke models in Section 5.6 will not be covered.)
 6 Oct 2020, Lecture 4: Finished Chapter 5 and most of Chapters
6 and 7. The formal property section (6.6) will be skipped.
 13 Oct 2020, Lecture 5: I lectured on the remaining parts
of Chapters 6 and 7, a few sections of Chapter 8, and discussed some
examples given in Chapter 9. This lecture was conducted via
Zoom. The two sets of slides are available:
first and second.
Exam
The exam that covers my lectures will be held on 8 December 2020
and will last 90 minutes. The exam will be administered using
online video.
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.).
 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 JeanYves 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.
 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.

Logic, Higherorder, by Dale Miller.
A short article for the
Encyclopedia of Artificial Intelligence: Second Edition,
edited by S. Shapiro, 1992.
(DVI,
PDF).

Programming
with HigherOrder 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.