15-317: Constructive Logic (Fa'15)

Schedule

There may be occasional supplemental handouts on lecture material, but you are expected to attend and take notes.

Date		Lecture Notes	Extra	Due
Tue	09/01	Overview
Wed	09/02	Rec: Propositions, judgements, proofs	TeX
Thu	09/03	Natural Deduction
Tue	09/08	Harmony		Asst 0
Wed	09/09	Rec: Harmonic tutch
Thu	09/10	Proofs as Programs
Tue	09/15	Quantification		Asst 1
Wed	09/16	Rec: Proof terms and verifications
Thu	09/17	Natural Numbers
Tue	09/22	Classical Logic		Asst 2
Wed	09/23	Rec: Recurse and arithmetic in tutch	Tutch
Thu	09/24	Classical Logic/Computation
Tue	09/29	Continuing Continuations		Asst 3
Wed	09/30	Rec: Review
Thu	10/01	Midterm I
Tue	10/06	Sequent Calculus		Asst 4
Wed	10/07	Rec: Natural deductions versus sequents
Thu	10/08	Cut Elimination
Tue	10/13	Quantifiers: Cut and Dependent Types	2.6,4.8	Asst 5
Wed	10/14	Rec: Eliminating cuts and dependent types
Thu	10/15	Inversion
Tue	10/20	Propositional Theorem Proving	extra	Asst 6
Wed	10/21	Rec: Proof search
Thu	10/22	Backward Logic Programming
Tue	10/27	Prolog	code
Wed	10/28	Rec: Programming in prolog	code
Thu	10/29	Prolog Programming Techniques	code	Asst 7
Tue	11/03	Unification
Wed	11/04	Rec: G4ip in prolog, review
Thu	11/05	Unification Resolution	extra
Tue	11/10	Midterm II
Wed	11/11	Rec: Growing trees and substituting blocks in Prolog	code
Thu	11/12	Operational Semantics	more
Tue	11/17	Forward Logic Programming
Wed	11/18	Rec: Unified logic programs forward		Asst 8
Thu	11/19	Forward Computation
Tue	11/24	Free: Optional: Exam-Problem-Solving Session
Wed	11/25	Free: Thanksgiving break
Thu	11/26	Free: Thanksgiving break
Tue	12/01	Linear Logic
Wed	12/02	Rec: Linearly forward
Thu	12/03	Linear Focusing	more	Asst 9
Tue	12/08	Substructural Operational Semantics	more	Asst 9½
Wed	12/09	Rec: Exam review
Thu	12/10	Exam review		Asst 10
Thu	12/17	Final Exam

The lecture schedule is tentative!

Assignment Schedule

	Points	Assignment		Due
Asst 0	10	Say hi to logic	code	Tue	09/08
Asst 1	40	Deduce, naturally	code	Tue	09/15
Asst 2	40	Come to terms with proofs	code	Tue	09/22
Asst 3	40	Pirates and quantifiers	code	Tue	09/29
Asst 4	20	Intuitions, classically and classical intuitions	code	Tue	10/06
Asst 5	40	Calculuate in sequents	code	Tue	10/13
Asst 6	40	Dependent types cut in	code	Tue	10/20
Asst 7	40	Inversion for proof search	code	Thu	10/29
Asst 8	40	Programming logically	code	Wed	11/18
Asst 9	40	Forward-looking prolog	code	Thu	12/03
Asst 9½	10	Exam reviewing		Tue	12/08
Asst 10	40	Linearized logic and logical linearities	code	Thu	12/10
Sum	400	points listed

The Assignment Schedule is tentative!
Homework assignments are due at start of lecture on the due day.