15-317 Constructive Logic

  • Lectures are Tuesday and Thursday in HH B131.
  • Recitations are Wednesday in SH 222 and GHC 5222
    Where a topic is not otherwise noted, recitations cover the material from the preceding two lectures.
  • There may be occasional supplemental handouts on lecture material, but you are expected to attend and take notes.
  • Lecture notes from a previous iteration of this course are available here.
  • The schedule is subject to change throughout the semester.
Date Lecture or Recitation    Homework Due

Tue Aug 26 Overview  
Thu Aug 28 Natural Deduction  

Tue Sep 2 Verifications and Uses  
Thu Sep 4 Harmony  

Tue Sep 9 Proofs as Programs  
Thu Sep 11 Sequent Calculus Homework 1

Tue Sep 16 Cut Elimination  
Thu Sep 18 Classical Logic Homework 2

Tue Sep 23 Classical Logic/Computation
Thu Sep 25 Double-Negation Translation Homework 3

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

Tue Oct 7 Theorem Proving: Inversion  
Thu Oct 9 Theorem Proving: G4IP  

Tue Oct 14 Logic Programming  
Thu Oct 16 Prolog Homework 5

Tue Oct 21 More Prolog, Higher-Order Logic Programming  
Thu Oct 23 Higher-Order Logic Programming Homework 6

Tue Oct 28 Higher-Order Logic Programming  
Thu Oct 30 Modal Logic Homework 7

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

Tue Nov 11 Monads/Lax Logic (Paper)  
Thu Nov 13 Linear Logic  

Tue Nov 18 Linear Logic  
Thu Nov 20 Focusing  

Tue Nov 25 Focusing  
Thu Nov 27 Thanksgiving break Homework 9

Tue Dec 2 Linear Logic Programming  
Thu Dec 4 Linear Logic Programming Homework 10

[ Home | Schedule | Assignments | Software ]