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 20222023, Miller's lectures will be on Mondays from 16h15  19h15.
Lectures will be in room 1002 in Bâtiment Sophie Germain.
Miller will lecture (in English) on the following five dates:
19, 26 September, 3, 10, 17 October.
Lecture Notes
Miller will be lecturing from his monograph
Proof theory, proof search, and logic programming.
 The current draft is dated 14
September 2022. This version will be used in class.
 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.
Important Dates
 19 Sep 2022, Lecture 1: The basics of sequent calculus. Chapters
1, 2, and 3 from Miller's lecture notes.
 26 Sep 2022, Lecture 2: Sequent calculus for classical and
intuitionistic logics. Chapter 4 and the start of Chapter 5.
 3 Oct 2022, Lecture 3: Goaldirected search, focused proofs in
intuitionistic logic, and logic programming examples. Most of Chapter
5 is covered (except Section 5.6 on Kripke models).
 10 Oct 2022, Lecture 4: Linear logic and logic programming: parts
of changes 6 and 7.
 17 Oct 2022, Lecture 5: Finish Chapters 6 and 7.
 12 Dec 2022, exam covering Miller's and Kesner's lectures.
Printed and personal documents are allowed. Computers and mobile
phones are not allowed.
Exam
The exam for my lectures will be held joint with Prof Kesner's
lectures. These exams will be on 12 December 2022 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 ProofTheoretic Foundations of Logic
Programming by Dale Miller.
To appear in the
20th
Anniversary Issue of the
Theory and Practice of Logic Programming (TPLP). Published online November 2021.
(doi,
arXiv,
HAL).
 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 foundation 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.