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:
Michele Pagani,
Delia Kesner,
Beniamino Accattoli,
and
Dale Miller.
Venue
During 2020, Miller's lectures will be on Monday from 16h15  19h15.
Lectures will be in room 1013 in Bâtiment Sophie Germain.
Miller will lecture (in English) on the following dates:
20 and 27 January and 3 February.
Gabriel Scherer will lecture
on 17 February instead of Miller.
Lecture Notes
The lecture notes for most of the Miller's lectures are collected in
the draft monograph ``Logic programming and its proof theory'' which
is available as a pdf.
Lectures
 20 Jan 2020, Lecture 1: Chapters 14, Sections 5.15.3 of
Chapter 5.
 27 Jan 2020, Lecture 2: Rest of Chapter 5 (skipping 5.7). Start
Chapter 7.
 3 Feb 2020, Lecture 3: Finished Chapters 7 and 8.
 10 Feb 2020, Lecture 4: Gabriel Scherer presented
these slides.
 2 Mar 2020, Second (final) exam. To prepare for Miller's part
of this exam, try the exercises in Chapters 4, 5, 7, 8.
Exam
The exam for the second part of this course will be on either 24
February or 2 March 2020. To prepare for the exam, read the lecture
notes and do the exercises in them.
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.