15-317 Constructive Logic

  • Lectures are Tuesday and Thursday in NSH 3002.
  • Recitations are Wednesday in PH A18B.
    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 28 Overview  
Thu Aug 30 Natural Deduction  

Tue Sep 4 Verifications and Uses  
Thu Sep 6 Harmony  

Tue Sep 11 Proofs as Programs  
Thu Sep 13 β-reduction and Substitution Homework 1

Tue Sep 18 Substitution and Sequent Calculus  
Thu Sep 20 Sequent Calculus Homework 2

Tue Sep 25 Cut Elimination  
Thu Sep 27 Cut Elimination Homework 3

Tue Oct 2 Classical Logic  
Thu Oct 4 Midterm I Homework 4

Tue Oct 9 Classical Logic/Computation  
Thu Oct 11 Theorem Proving: Inversion  

Tue Oct 16 Theorem Proving: G4IP  
Thu Oct 18 Logic Programming Homework 5

Tue Oct 23 Prolog  
Thu Oct 25 Typed Prolog / Higher-Order Logic Programming Homework 6

Tue Oct 30 Higher-Order Logic Programming  
Thu Nov 1 Total Logic Programming Homework 7

Tue Nov 6 Dependent Types  
Thu Nov 8 Midterm II Homework 8

Tue Nov 13 LF Type Theory  
Thu Nov 15 Higher-Order Abstract Syntax  

Tue Nov 20 Higher-Order Judgments  
Thu Nov 22 Thanksgiving Break (no classes)  

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

Tue Dec 4 Linear Logic  
Thu Dec 6 Linear Logic Homework 10

[ Home | Schedule | Assignments | Software ]