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.
DateLecture NotesExtraDue
Tue09/01Overview
Wed09/02Rec: Propositions, judgements, proofsTeX
Thu09/03Natural Deduction
Tue09/08HarmonyAsst 0 
Wed09/09Rec: Harmonic tutch
Thu09/10Proofs as Programs
Tue09/15QuantificationAsst 1 
Wed09/16Rec: Proof terms and verifications
Thu09/17Natural Numbers
Tue09/22Classical LogicAsst 2 
Wed09/23Rec: Recurse and arithmetic in tutchTutch
Thu09/24Classical Logic/Computation
Tue09/29Continuing ContinuationsAsst 3 
Wed09/30Rec: Review
Thu10/01Midterm I
Tue10/06Sequent CalculusAsst 4 
Wed10/07Rec: Natural deductions versus sequents
Thu10/08Cut Elimination
Tue10/13Quantifiers: Cut and Dependent Types2.6,4.8Asst 5 
Wed10/14Rec: Eliminating cuts and dependent types
Thu10/15Inversion
Tue10/20Propositional Theorem ProvingextraAsst 6 
Wed10/21Rec: Proof search
Thu10/22Backward Logic Programming
Tue10/27Prologcode 
Wed10/28Rec: Programming in prologcode 
Thu10/29Prolog Programming Techniquescode Asst 7 
Tue11/03Unification
Wed11/04Rec: G4ip in prolog, review
Thu11/05Unification Resolutionextra
Tue11/10Midterm II
Wed11/11Rec: Growing trees and substituting blocks in Prologcode 
Thu11/12Operational Semanticsmore
Tue11/17Forward Logic Programming
Wed11/18Rec: Unified logic programs forwardAsst 8 
Thu11/19Forward Computation
Tue11/24Free: Optional: Exam-Problem-Solving Session
Wed11/25Free: Thanksgiving break
Thu11/26Free: Thanksgiving break
Tue12/01Linear Logic
Wed12/02Rec: Linearly forward
Thu12/03Linear FocusingmoreAsst 9 
Tue12/08Substructural Operational SemanticsmoreAsst 9½ 
Wed12/09Rec: Exam review
Thu12/10Exam reviewAsst 10 
Thu12/17Final Exam
The lecture schedule is tentative!

Assignment Schedule

PointsAssignmentDue
Asst 010Say hi to logiccode,solTue 09/08
Asst 140Deduce, naturallycode,solTue 09/15
Asst 240Come to terms with proofscode,solTue 09/22
Asst 340Pirates and quantifierscode,solTue 09/29
Asst 420Intuitions, classically and classical intuitionscode,solTue 10/06
Asst 540Calculuate in sequentscode,solTue 10/13
Asst 640Dependent types cut incode,solTue 10/20
Asst 740Inversion for proof searchcodeThu 10/29
Asst 840Programming logicallycodeWed 11/18
Asst 940Forward-looking prologcodeThu 12/03
Asst 9½10Exam reviewingTue 12/08
Asst 1040Linearized logic and logical linearitiescodeThu 12/10
Sum400points listed

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