15-317 Constructive Logic
Schedule

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
Wed	Aug	29	Clue
Thu	Aug	30	Natural Deduction

Tue	Sep	4	Verifications and Uses
Wed	Sep	5	Tutch
Thu	Sep	6	Harmony

Tue	Sep	11	Proofs as Programs
Wed	Sep	12	Soundness and Completeness
Thu	Sep	13	β-reduction and Substitution	Homework 1

Tue	Sep	18	Substitution and Sequent Calculus
Wed	Sep	19	Quantifiers
Thu	Sep	20	Sequent Calculus	Homework 2

Tue	Sep	25	Cut Elimination
Wed	Sep	26	Natural Numbers
Thu	Sep	27	Cut Elimination	Homework 3

Tue	Oct	2	Classical Logic
Wed	Oct	3	Midterm Review
Thu	Oct	4	Midterm I	Homework 4

Tue	Oct	9	Classical Logic/Computation
Wed	Oct	10	Midterm Review
Thu	Oct	11	Theorem Proving: Inversion

Tue	Oct	16	Theorem Proving: G4IP
Wed	Oct	17	Theorem Prover Discussion
Thu	Oct	18	Logic Programming	Homework 5

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

Tue	Oct	30	Higher-Order Logic Programming
Wed	Oct	31	G4IP in Prolog
Thu	Nov	1	Total Logic Programming	Homework 7

Tue	Nov	6	Dependent Types
Wed	Nov	7	Midterm Review
Thu	Nov	8	Midterm II	Homework 8

Tue	Nov	13	LF Type Theory
Wed	Nov	14	Midterm Review
Thu	Nov	15	Higher-Order Abstract Syntax

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

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

Tue	Dec	4	Linear Logic
Wed	Dec	5	Linear Logic Review
Thu	Dec	6	Linear Logic	Homework 10

[ Home | Schedule | Assignments | Software ]