15-399, 80-317/617
Constructive Logic
Schedule

Lectures are Mondays and Wednesdays in DH A317.
Recitations are Fridays in DH A317.
Recitations generally cover the material from the preceding two lectures, along with past and current homework.
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

Mon	Aug	27	Introduction	intro.pdf

Wed	Aug	29	Judgments and Propositions	prop.pdf

Fri	Aug	31	Pre-Test

Wed	Sep	5	Disjunction and Negation	disjunction.pdf

Mon	Sep	10	Notational Definition	notational.pdf

Wed	Sep	12	Classical Semantics	Huth + Ryan 1.4

Mon	Sep	17	Kripke Semantics	Handout	Assignment 1

Wed	Sep	19	Soundness and Completeness	Handout

Mon	Sep	24	Normal Deductions	normal.pdf	Assignment 2

Wed	Sep	26	Proofs as Programs	pap.pdf

Mon	Oct	1	The Curry-Howard Isomorphism	curry.pdf	Assignment 3

Wed	Oct	3	Lambda Calculus	lambda.pdf

Mon	Oct	8	Normalization	Handout	Assignment 4

Wed	Oct	10	Midterm Exam 1

Mon	Oct	15	Primitive Recursion	primitive.pdf

Wed	Oct	17	Data Types	data.pdf

Mon	Oct	22	Midsemester Break

Wed	Oct	24	Trees		Assignment 5

Mon	Oct	29	Predicates	predicates.pdf	Assignment 5 - extra credit

Wed	Oct	31	Quantifiers	quantifiers.pdf

Mon	Nov	5	Classical versus Constructuve Logic	classical.pdf	Assignment 6

Wed	Nov	7	Midterm Exam 2

Mon	Nov	12	First-Order Logic	fol.pdf	Assignment 6 - extra credit

Wed	Nov	14	Classical and Constructive Validity	Huth + Ryan 2.2-4	Assignment 7

Mon	Nov	19	Arithmetic	arithmetic.pdf

Wed	Nov	21	Thanksgiving Break

Mon	Nov	26	Contracting Proofs	contract.pdf

Wed	Nov	28	Conditions for Contraction		Assignment 8

Mon	Dec	3	Structural Induction	structure.pdf	Assignment 9

Wed	Dec	5	Dependent Types	depend.pdf

Mon	Dec	10	Propositions as Types	pat.pdf	Assignment 10