15-317: Constructive Logic (Sp'20)


There may be occasional supplemental handouts on lecture material, but you are expected to attend and take notes.
DateLecture NotesExtraDue
Wed01/15Rec: Propositions, judgements, proofs
Thu01/16Natural Deduction
Tue01/21HarmonyHW 0 
Wed01/22Rec: Harmonic tutch
Thu01/23Classical Logic
Tue01/28Proofs as ProgramsHW 1 
Wed01/29Rec: Proof terms and verifications
Tue02/04Natural NumbersHW 2 
Wed02/05Rec: Recurse and arithmetic in tutch
Thu02/06Sequent Calculus
Tue02/11ReviewHW 3 
Wed02/12Rec: Natural deductions versus sequents
Thu02/13?Midterm I?
Tue02/18Cut Elimination
Wed02/19Rec: Sequents and KeYmaera I
Tue02/25Propositional Theorem ProvingHW 4 
Wed02/26Rec: Playing with proof systems
Thu02/27Quantifiers: Cut and Dependent Types,
Tue03/03Backward Logic ProgrammingHW 5 
Wed03/04Rec: Quantifiers and logic programming
Tue03/10Free: Spring breakHW 6 
Wed03/11Free: Spring break
Thu03/12Free: Spring break
Tue03/17Prolog Programming TechniquesHW 7 
Wed03/18Rec: Programming in prolog
Thu03/19Operational Semantics
Tue03/24UnificationHW 8 
Wed03/25Rec: Prolog techniques, semantics, and unification
Thu03/26Unification Resolution
Tue03/31ReviewHW 8½ 
Wed04/01Rec: Pre-exam review and some more Prolog
Thu04/02?Midterm II?
Tue04/07Forward Logic Programming
Wed04/08Rec: Unified logic programs forward
Thu04/09Forward Computation
Thu04/16Free: No classHW 9 
Tue04/21Linear Logic
Wed04/22Rec: Linearly lining up for food
Thu04/23Linear FocusingHW 10 
Tue04/28Substructural Operational Semantics
Wed04/29Rec: Exam review
Final Exam
The lecture schedule is tentative!

Assignment Schedule

HW 010Say hi to logicTue01/21
HW 140Deduce, naturally and harmoniouslyTue01/28
HW 240Come to terms with proofsTue02/04
HW 340Quantify proofs with dataTue02/11
HW 440Calculuate in sequentsTue02/25
HW 540Propositional theorem provingTue03/03
HW 640Sequential quantifiers and being logical about programmingTue03/10
HW 740Practicing prolog programmingTue03/17
HW 820Programming logicallyTue03/24
HW 8½20Programming more logicallyTue03/31
HW 940Forward logic programmingThu04/16
HW 1030Let's be linearThu04/23
Sum400points listed

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