Date  Lecture  Homework  



We  Sep  5  Overview/Natural Deduction  
Fr  Sep  7  Natural Deduction  


Mo  Sep  10  Tutorial (Maja)  
We  Sep  12  Tutorial (Maja)  
Fr  Sep  14  Normal Proofs  HW 1 out /  


Mo  Sep  17  Notational definitions  
We  Sep  19  ProofsasPrograms (1)  
Fr  Sep  21  ProofsasPrograms  HW 1 due / HW 2 out  


Mo  Sep  24  Properties of proof terms  
We  Sep  26  Lambdacalculus  
Fr  Sep  28  Primitive recursion  HW 2 due / HW 3 out  


Mo  Oct  1  Datatypes  
We  Oct  3  Induction  
Fr  Oct  5  to be announced  HW 3 due / HW 4 out  


Mo  Oct  8  Thanksgiving Holiday  
Tu  Oct  9  Firstorder logic  
We  Oct  10  Firstorder logic  
Fr  Oct  12  Firstorder logic  HW 4 due / HW 5 out  


Mo  Oct  15  Contracting proofs  
We  Oct  17  Reasoning about data  
Fr  Oct  19  Review  HW 5 due  


Mo  Oct  22  Midterm  
We  Oct  24  Normal natural deduction  
Fr  Oct  26  Consistency  


Mo  Oct  29  Sequent Calculus  
We  Oct  31  Metatheoretic properties  
Fr  Nov  2  Inversion and focusing  Project Proposal due  


Mo  Nov  5  Guided theorem prover  
We  Nov  7  Logic Programming  
Fr  Nov  9  Logic Programming  


Mo  Nov  12  Forward theorem proving  
We  Nov  14  Forward theorem proving  
Fr  Nov  16  Bidirectional theorem proving  Project Milestone  


Mo  Nov  19  Special topic: Modal logic  
We  Nov  21  Special topic: Dependent types  
Fr  Nov  23  Special topic: Linear logic  


Mo  Nov  26  Presentations  
We  Nov  28  Presentations  
Fr  Nov  30  Presentations  


Mo  Dec  3  Presentations  
