15-317 Constructive Logic

  • 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 Additional Material Homework Out/Due

Mon Aug 27 Overview
Wed Aug 29 Natural Deduction

Mon Sep 3 Labor Day Holiday
Wed Sep 5 Harmony

Mon Sep 10 Proofs as Programs
Wed Sep 12 Verifications

Mon Sep 17 Quantification
Wed Sep 19 Induction and Recursion extracted functions

Mon Sep 24 Heyting Arithmetic
Wed Sep 26 Sequent Calculus

Mon Oct 1 Midterm I practice midterm 1 (sol) practice midterm 2 (sol)
Wed Oct 3 Cut Elimination

Mon Oct 8 Propositional Theorem Proving
Wed Oct 10 Inversion

Mon Oct 15 Certifying Theorem Provers
Wed Oct 17 Logic Programming

Mon Oct 22 Prolog examples
Wed Oct 24 Types as Predicates

Mon Oct 29 Chaining meta-interpreter
Wed Oct 31 Datalog

Mon Nov 5 Focusing rule summary
Wed Nov 7 Midterm II practice midterm (sol)

Mon Nov 12 Substructural Deduction
Wed Nov 14 Ordered Logic

Mon Nov 19 Modal Logic further reading
Wed Nov 21 Thanksgiving Holiday

Mon Nov 26 Subsingleton Logic Homework 10 Due
Wed Nov 28 Ordered Proofs as Concurrent Programs

Mon Dec 3 Martin-Löf Type Theory rule summary
Wed Dec 5 Review board

Tue Dec 11 Final 1pm-4pm, POS A35 practice (sol)

[ Home | Schedule | Assignments | Software ]

Ankush Das