Home
Schedule
Assignments
Handouts
Software
 
academic.cs.15-317
 
fp@cs
Frank Pfenning
  

15-317 Constructive Logic
Schedule

  • Lectures are Tuesday and Thursday in Baker 255A.
  • Recitations are Wednesday in SH 214.
    Recitations generally cover the material from the preceding two lectures.
  • The class notes provide additional reading material.
    They complement, but do not replace the lecture.
  • The schedule is subject to change throughout the semester.
Date Lecture or Recitation    Reading    Homework Due
Tue Aug 26 Overview 01-overview.pdf  
Wed Aug 27 Clue 01.pdf, class.pdf  
Thu Aug 28 Natural Deduction 02-natded.pdf  
Tue Sep 2 Harmony 03-harmony.pdf  
Wed Sep 3 Tutch notes, Tutch code  
Thu Sep 4 Proofs as Programs 04-pap.pdf  
Tue Sep 9 Subject Reduction 05-subred.pdf  
Wed Sep 10 Proof terms and reduction  
Thu Sep 11 Quantification 06-quant.pdf Homework 1
Tue Sep 16 Computational Meaning of Quantifiers 07-compq.pdf  
Wed Sep 17 Homework 1 Solutions, Proof terms    
Thu Sep 18 Proof Irrelevance 08-irrelevance.pdf Homework 2
Tue Sep 23 Classical Logic 09-10-classical.pdf  
Wed Sep 24 Truth Tables 09-10-classical.pdf  
Thu Sep 25 Classical Computation 09-10-classical.pdf Homework 3
Tue Sep 30 Classical Quantifiers    
Wed Oct 1 Review    
Thu Oct 2 Midterm I   Homework 4
Tue Oct 7 Induction    
Wed Oct 8 Midterm Answers, Induction    
Thu Oct 9 Induction    
Tue Oct 14 Logic Programming 01-lp.pdf code  
Wed Oct 15 Induction    
Thu Oct 16 Logic Programming, Control Operators 02-data.pdf code Homework 5
Tue Oct 21 Theorem Proving    
Wed Oct 22 Sorting code  
Thu Oct 23 Theorem Proving   Homework 6
Tue Oct 28 Sequent Calculus seqcalc.pdf  
Wed Oct 29 Proofs of Identity and Cut    
Thu Oct 30 Meta-interpreters   Homework 7
Tue Nov 4 No Class    
Wed Nov 5 Review    
Thu Nov 6 Midterm II    
Tue Nov 11 Bottom-up logic programming 20-bottomup.pdf Homework 8
Wed Nov 12 Model checking    
Thu Nov 13 Bottom-up logic programming    
Tue Nov 18 Linear logic programming 12-linear.pdf  
Wed Nov 19 Linear logic programming    
Thu Nov 20 Linear logic    
Tue Nov 25 Reading Day (no class)   Homework 9
Wed Nov 26 Thanksgiving Holiday    
Thu Nov 27 Thanksgiving Holiday    
Tue Dec 2 Lax Logic and Effects    
Wed Dec 3 Purely Functional Effects errors, environments  
Thu Dec 4 Authorization Logic   Homework 10
Final, Tue Dec 9, 8:30am-11:30am, PH A19    

[ | Schedule | Assignments | Handouts | Software ]

fp@cs
Frank Pfenning