
15317 Constructive Logic

Date  Lecture or Recitation  Homework Due  



Tue  Aug  28  Overview  
Wed  Aug  29  Clue  
Thu  Aug  30  Natural Deduction  


Tue  Sep  4  Verifications and Uses  
Wed  Sep  5  Tutch  
Thu  Sep  6  Harmony  


Tue  Sep  11  Proofs as Programs  
Wed  Sep  12  Soundness and Completeness  
Thu  Sep  13  βreduction and Substitution  Homework 1  


Tue  Sep  18  Substitution and Sequent Calculus  
Wed  Sep  19  Quantifiers  
Thu  Sep  20  Sequent Calculus  Homework 2  


Tue  Sep  25  Cut Elimination  
Wed  Sep  26  Natural Numbers  
Thu  Sep  27  Cut Elimination  Homework 3  


Tue  Oct  2  Classical Logic  
Wed  Oct  3  Midterm Review  
Thu  Oct  4  Midterm I  Homework 4  


Tue  Oct  9  Classical Logic/Computation  
Wed  Oct  10  Midterm Review  
Thu  Oct  11  Theorem Proving: Inversion  


Tue  Oct  16  Theorem Proving: G4IP  
Wed  Oct  17  Theorem Prover Discussion  
Thu  Oct  18  Logic Programming  Homework 5  


Tue  Oct  23  Prolog  
Wed  Oct  24  Prolog  
Thu  Oct  25  Typed Prolog / HigherOrder Logic Programming  Homework 6  


Tue  Oct  30  HigherOrder Logic Programming  
Wed  Oct  31  G4IP in Prolog  
Thu  Nov  1  Total Logic Programming  Homework 7  


Tue  Nov  6  Dependent Types  
Wed  Nov  7  Midterm Review  
Thu  Nov  8  Midterm II  Homework 8  


Tue  Nov  13  LF Type Theory  
Wed  Nov  14  Midterm Review  
Thu  Nov  15  HigherOrder Abstract Syntax  


Tue  Nov  20  HigherOrder Judgments  
Wed  Nov  21  Thanksgiving Break (no classes)  
Thu  Nov  22  Thanksgiving Break (no classes)  


Tue  Nov  27  Logic Programming in Elf  
Wed  Nov  28  Logic Programming in Elf  
Thu  Nov  29  Twelf  Homework 9  


Tue  Dec  4  Linear Logic  
Wed  Dec  5  Linear Logic Review  
Thu  Dec  6  Linear Logic  Homework 10  
[ Home  Schedule  Assignments  Software ]