15-317: Constructive Logic (Fa'16)

Schedule

There may be occasional supplemental handouts on lecture material, but you are expected to attend and take notes.
DateLecture NotesExtraDue
Tue08/30Overview
Wed08/31Rec: Propositions, judgements, proofscode 
Thu09/01Natural Deduction
Tue09/06HarmonyHW 0 
Wed09/07Rec: Harmonic tutch
Thu09/08Classical Logic
Tue09/13Proofs as ProgramsHW 1 
Wed09/14Rec: Proof terms and verificationscode 
Thu09/15Quantification
Tue09/20Natural NumbersHW 2 
Wed09/21Rec: Recurse and arithmetic in tutch
Thu09/22Sequent Calculus
Tue09/27ReviewHW 3 
Wed09/28Rec: Natural deductions versus sequents
Thu09/29Midterm I
Tue10/04Cut Elimination
Wed10/05Rec: Sequents and KeYmaera Icode 
Thu10/06Inversion
Tue10/11Propositional Theorem ProvingextraHW 4 
Wed10/12Rec: Playing with proof systemssol
Thu10/13Quantifiers: Cut and Dependent Types2.6,4.8
Tue10/18Backward Logic Programmingcode HW 5 
Wed10/19Rec: Quantifiers and logic programming
Thu10/20Prologcode 
Tue10/25Prolog Programming Techniquescode HW 6 
Wed10/26Rec: Programming in prologcode 
Thu10/27Operational Semanticsmore
Tue11/01UnificationHW 7 
Wed11/02Rec: Prolog techniques, semantics, and unificationcode 
Thu11/03Unification Resolutionextra
Tue11/08ReviewHW 8 
Wed11/09Rec: Pre-exam review and some more Prologcode 
Thu11/10Midterm II
Tue11/15Forward Logic Programmingcode HW 8½ 
Wed11/16Rec: Unified logic programs forward
Thu11/17Forward Computationcode 
Tue11/22Free: Optional: Resolution
Wed11/23Free: Thanksgiving break
Thu11/24Free: Thanksgiving break
Tue11/29Linear Logic
Wed11/30Rec: Linearly lining up for food
Thu12/01Linear FocusingmoreHW 9 
Tue12/06Substructural Operational Semantics
Wed12/07Rec: Exam review
Thu12/08ReviewHW 10 
Fri12/16Final Exam
The lecture schedule is tentative!

Assignment Schedule

PointsAssignmentDue
HW 010Say hi to logiccodeTue09/06
HW 140Deduce, naturally and harmoniouslycodeTue09/13
HW 240Come to terms with proofscodeTue09/20
HW 340Quantify proofs with datacodeTue09/27
HW 440Calculuate in sequentscodeTue10/11
HW 540Propositional theorem provingcodeTue10/18
HW 640Sequential quantifiers and being logical about programmingcodeTue10/25
HW 740Practicing prolog programmingcodeTue11/01
HW 820Programming logicallycodeTue11/08
HW 8½20Programming more logicallycodeTue11/15
HW 940Forward logic programmingThu12/01
HW 1030Let's be linearcodeThu12/08
Sum400points listed

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