
15317 Constructive Logic

Date  Lecture or Recitation  Homework Due  



Tue  Aug  26  Overview  
Wed  Aug  27  Clue  
Thu  Aug  28  Natural Deduction  


Tue  Sep  2  Verifications and Uses  
Wed  Sep  3  Tutch (recitation a) (recitation b)  
Thu  Sep  4  Harmony  


Tue  Sep  9  Proofs as Programs  
Wed  Sep  10  Soundness and Completeness  
Thu  Sep  11  Sequent Calculus  Homework 1  


Tue  Sep  16  Cut Elimination  
Wed  Sep  17  Quantifiers  
Thu  Sep  18  Classical Logic  Homework 2  


Tue  Sep  23  Classical Logic/Computation  
Wed  Sep  24  Review/Natural Numbers  
Thu  Sep  25  DoubleNegation Translation  Homework 3  


Tue  Sep  30  Friedman's Trick  
Wed  Oct  1  Midterm Review  
Thu  Oct  2  Midterm I  Homework 4  


Tue  Oct  7  Theorem Proving: Inversion  
Wed  Oct  8  Midterm Recap  
Thu  Oct  9  Theorem Proving: G4IP  


Tue  Oct  14  Logic Programming  
Wed  Oct  15  Theorem Prover Discussion  
Thu  Oct  16  Prolog  Homework 5  


Tue  Oct  21  More Prolog, HigherOrder Logic Programming  
Wed  Oct  22  G4IP in Prolog  
Thu  Oct  23  HigherOrder Logic Programming  Homework 6  


Tue  Oct  28  HigherOrder Logic Programming  
Wed  Oct  29  Review of Twelf  
Thu  Oct  30  Modal Logic  Homework 7  


Tue  Nov  4  Modal Logic (Related paper)  
Wed  Nov  5  Midterm Review  
Thu  Nov  6  Midterm II  Homework 8  


Tue  Nov  11  Monads/Lax Logic (Paper)  
Wed  Nov  12  Modal Logic and Runtime Code Generation  
Thu  Nov  13  Linear Logic  


Tue  Nov  18  Linear Logic  
Wed  Nov  19  Linear Logic Review  
Thu  Nov  20  Focusing  


Tue  Nov  25  Focusing  
Wed  Nov  26  Thanksgiving break  
Thu  Nov  27  Thanksgiving break  Homework 9  


Tue  Dec  2  Linear Logic Programming  
Wed  Dec  3  Linear Logic Programming Examples  
Thu  Dec  4  Linear Logic Programming  Homework 10  
[ Home  Schedule  Assignments  Software ]