15-399 Constructive Logic
Handouts

The handout Constructive Logic contains a complete set of notes as of the indicated date.
This includes all incremental handouts with possible corrections and updates.
Note that I do not correct incremental handouts on-line.

In the latter part of the course, we will be using the textbook by Huth & Ryan listed below. Copies of the relevant sections will be handed out in class and be available from the class assistant Maury Burgwin in Wean Hall 8124.

Logic in Computer Science Modelling and Reasoning about Systems: Michael Huth and Mark Ryan,
Cambridge University Press, 2000.

Date	Handout	Note

Dec 28	Constructive Logic	Complete set of notes for Lectures 1-24, except Lectures 7, 8, and 23
Sep 21	Classical and Constructive Logic	Notes on Lectures 7 and 8 by Jeremy Avigad

Aug 29	Introduction	Lecture 1
Aug 31	Propositional Logic	Lecture 2
Sep 5	Notational Definition	Lecture 3
Sep 7	Linear and Normal Deductions	Lecture 4
Sep 12	Proofs as Programs	Lecture 5
Sep 14	Subject Reduction	Lecture 6
Sep 21	Classical and Constructive Logic	Lecture 7, Lecture 8
Sep 26	Primitive Recursion	Lecture 9
Sep 28	Lists and Predicates	Lecture 10
Oct 6	Induction and Quantification	Lecture 11
Oct 14	First-Order Logic	Lecture 12
Oct 16	Arithmetic	Lecture 13
Oct 20	Contracting Proofs to Programs	Lecture 14
Oct 20	Structural Induction	Lecture 15
Oct 24	Reasoning about Data Representations	Lecture 16
Oct 31	Complete Induction	Lecture 17
Nov 3	Dependent Types	Lecture 18, Lecture 19
Nov 6	Data Structure Invariants	Lecture 19, Lecture 20
Dec 13	Decidable Fragments	Lecture 21, Lecture 22, Lecture 24

fp@cs
Frank Pfenning

15-399 Constructive Logic Handouts

15-399 Constructive Logic
Handouts