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	25	Overview
Tue	Aug	26	Recitation
Wed	Aug	27	Natural Deduction		HW1 out

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

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

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

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

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

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

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

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

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

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

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

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

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

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

TBA			Final exam

[ Home | Schedule | Assignments | Software ]