15-317: Constructive Logic (Fa'15)

  1. Home
  2. >>
  3. Courses
  4. >>
  5. ConstLog. Fa15
  6. >>
  7. Schedule


There may be occasional supplemental handouts on lecture material, but you are expected to attend and take notes.
DateLecture NotesExtraDue
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
Tue10/20Propositional Theorem ProvingextraAsst 6 
Wed10/21Rec: Proof search
Thu10/22Backward Logic Programming
Wed10/28Rec: Programming in prologcode 
Thu10/29Prolog Programming Techniquescode Asst 7 
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

Asst 010Say hi to logiccodeTue09/08
Asst 140Deduce, naturallycodeTue09/15
Asst 240Come to terms with proofscodeTue09/22
Asst 340Pirates and quantifierscodeTue09/29
Asst 420Intuitions, classically and classical intuitionscodeTue10/06
Asst 540Calculuate in sequentscodeTue10/13
Asst 640Dependent types cut incodeTue10/20
Asst 740Inversion for proof searchcodeThu10/29
Asst 840Programming logicallycodeWed11/18
Asst 940Forward-looking prologcodeThu12/03
Asst 9½10Exam reviewingTue12/08
Asst 1040Linearized logic and logical linearitiescodeThu12/10
Sum400points listed

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