Logique linéaire et paradigmes logiques du calcul

Course 2-1 offered within MPRI.

A brief discription of this course is available in French.

Instructors

Instructors: Dale Miller, Delia Kesner, and Beniamino Accattoli.

Venue

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.

Lecture Notes

Two sets of lecture notes will be consulted during Miller's lectures.

1. Proof search, proof theory, and logic programming by Miller. We will only cover Chapters 1-7, and 9. 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.
   1. Draft version on 22 Sept 2021. We will cover the first five chapters during the first two lectures.
   2. Chapters 6 and 7 on linear logic programming will appear by the third lecture.
2. Introduction to Linear Logic by Roberto Di Cosmo and Vincent Danos will be referenced for some lectures.

Lectures

• 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.
• 6 Oct 2021, Lecture 3:
• 13 Oct 2021, Lecture 4:
• 20 Oct 2021, Lecture 5:

Exam

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.

1. Linear Logic, by Roberto Di Cosmo and Dale Miller, The Stanford Encyclopedia of Philosophy (Winter 2016 Edition), Edward N. Zalta (ed.).
2. 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.
3. 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. Also available here.
4. 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.
5. Logic, Higher-order, by Dale Miller. A short article for the Encyclopedia of Artificial Intelligence: Second Edition, edited by S. Shapiro, 1992. (DVI, PDF).
   
6. Programming with Higher-Order 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.