15-317 Constructive Logic
Schedule

The class notes provide additional reading material. They complement the lecture, but do not replace it.
The schedule (including exam dates) is subject to change throughout the semester.

Date			Lecture or Recitation	Additional Material	Homework Due/Out

Mon	Aug	26	Overview
Tue	Aug	27	Recitation
Wed	Aug	28	Natural Deduction		HW1 out

Mon	Sep	2	No class
Tue	Sep	3	Recitation
Wed	Sep	4	Harmony		HW1 due, HW2 out

Mon	Sep	9	Proofs as Programs
Tue	Sep	10	Recitation: Proofs as ML programs
Wed	Sep	11	Verifications and Uses		HW2 due, HW3 out

Mon	Sep	16	Quantification
Tue	Sep	17	Recitation
Wed	Sep	18	Heyting Arithmetic		HW3 due, HW4 out

Mon	Sep	23	Sequent Calculus
Tue	Sep	24	Recitation: Admissibility and derivability
Wed	Sep	25	Sequent Calculus		HW4 due, HW5 out

Mon	Sep	30	Midterm 1
Tue	Oct	1	Recitation: Exam recap
Wed	Oct	2	Cut Elimination		HW5 due, HW6 out

Mon	Oct	7	Propositional Theorem Proving
Tue	Oct	8	Recitation
Wed	Oct	9	Inversion		HW6 due, HW7 out

Mon	Oct	14	No class
Tue	Oct	15	No recitation
Wed	Oct	16	No class

Mon	Oct	21	Classical Logic
Tue	Oct	22	Recitation: Kolmogorov translation
Wed	Oct	23	Logic Programming		HW7 due, HW8 out

Mon	Oct	28	Prolog
Tue	Oct	29	Recitation: Practical Prolog
Wed	Oct	30	Backward Chaining		HW8 due, HW9 out

Mon	Nov	4	Forward Chaining
Tue	Nov	5	No recitation
Wed	Nov	6	Linear Logic	(Blocks World, Substructural Deduction)	HW9 due, HW10 out

Mon	Nov	11	Midterm 2
Tue	Nov	12	Recitation: Exam recap
Wed	Nov	13	Focusing		HW10 due, HW11 out

Mon	Nov	18	Modal Logic
Tue	Nov	19	Recitation: Linear logic applications		HW11 due, HW12 out
Wed	Nov	20	Ordered Logic

Mon	Nov	25	Session Types
Tue	Nov	26	Recitation: Lax logic and monads		HW12 due
Wed	Nov	27	No class

Mon	Dec	2	Classical Sequent Calculus
Tue	Dec	3	Recitation: Certifying Theorem Provers
Wed	Dec	4	TBA

TBA			Final exam

[ Home | Schedule | Assignments | Software ]