A graduate course:
Proof systems for linear, intuitionistic, and classical logic
Venue
Dale
Miller lectures for 20 hours during the weeks after Easter at
the Dipartimento di Informatica, Università Ca' Foscari Venezia.
 15 April: 10h00  13h00. Chapters 1 and 2 of lecture notes.
 16 April: 10h00  13h00. Chapter 3.
Exercises to be discussed in class Monday, 20 April: 8, 9, 12
(solution in handout), 18, 19, 21.
 17 April: No lectures today. Hours have been moved to the
following week.
 20 April: 10h00  13h00: Chapter 4 (hc, hh)
 21 April: 10h00  13h00: Chapter 5 (backchaining)
 22 April: 10h00  13h00: Chapter 6 (linear logic)
 23 April: 10h00  13h00: Chapter 6 (linear logic programming)
 24 April: 11h00  13h00: Other topics:
Encryption as an abstract
datatype and
Focusing and Polarization in
Intuitionistic Logic.
Topics

Sequent calculus for classical and intuitionistic logics. Basic
results about uniform proof. A
proof theory foundation"for mooic programming.

Sequent calculus for linear logic. Generalize uniform proof and
show new possibilities for logic programming.

Focused proof systems for linear, intuitionistic, and classical
logic.

If time permits, applications of focusing proofs will be presented:
Herbrand's theorem, model checking, theorem proving with induction
and coinduction, etc.
Exam / Evaluation
The exam for the course should be returned
to Miller by 15 May 2009.
Five students have taken the exam: Raju Halder, Luca Leonardi, Andrea
Petrucci, Andrea Triossi, Matteo Zanioli.
References and Links
Lecture notes are available as pdf. Please
have a copy of these available in order to follow the lectures.
Below are some documents available via the web that may be of use
in this class.

Two recent papers that provide flexible focused proof systems for
intuitionistic and classical proof systems. A conference
paper (CSL'07):
Focusing and Polarization in Intuitionistic Logic by Chuck Liang and Dale
Miller (pdf, slides).
An extended, journal version of that work:
Focusing and Polarization in Linear, Intuitionistic, and Classical
Logic by Chuck Liang and Dale Miller. Accepted (March 2008) to TCS.
Draft dated May 2008: (pdf).
 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.
 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.
 Linear
Logic
by Roberto
Di Cosmo and Dale Miller. The Stanford
Encyclopedia of Philosophy (Fall 2006 Edition), Edward N. Zalta (ed.).