Week

Class

HW

Book

Aug 27

Preface.v, Basics.v, _CoqProject

Basics.v, BasicsTest.v, Makefile

Logical Foundations

Aug 29

Induction.v, Lists.v

Induction.v, InductionTest.v, Lists.v (No HW)

Logical Foundations

Sep 03

Poly.v, Tactics.v

Poly.v, Tactics.v, PolyTest.v, TacticsTest.v

Logical Foundations

Sep 05

Logic.v

NO Logic HW this week

Logical Foundations

Sep 10

"Continue Logic"

Logic.v, LogicTest.v

Logical Foundations

Sep 12

IndProp.v

IndProp.v, IndPropTest.v

Logical Foundations

Sep 17

ProofObjects.v, IndPrinciples.v

ProofObjects.v, IndPrinciples.v, ProofObjectsTest.v, IndPrinciplesTest.v

Logical Foundations

Sep 19

AltAuto.v

AltAuto.v (No HW)

Logical Foundations

Sep 24

Imp.v, Maps.v

Maps.v, MapsTest.v, Imp.v, ImpTest.v

Logical Foundations

PLF Setup

Maps.v, Imp.v, Makefile, _CoqProject

Programming Language Foundations

Sep 26

Equiv.v

Programming Language Foundations

Oct 01

Equiv.v, EquivTest.v

Programming Language Foundations

Oct 03

Hoare.v

Hoare.v, HoareTest.v

Programming Language Foundations

Oct 08

Hoare2.v

Hoare2.v (No HW)

Programming Language Foundations

Oct 10

Smallstep.v

Smallstep.v,SmallstepTest.v

Programming Language Foundations

Oct 15

Types.v

Types.v, TypesTest.v

Programming Language Foundations

Oct 17

Stlc.v

Stlc.v

Programming Language Foundations

Oct 22

Midterm Review

Fall 19 (w/ solutions), Fall 20 (no solutions), Fall 22 (no solutions), Fall 23 (no solutions)

QuickChick

Oct 24

MIDTERM

Oct 29

StlcProp.v

StlcProp.v

PLF

Oct 31

Typeclasses.v

Introduction.v,Typeclasses.v

QC

Nov 5

QC.v

QC.v

QC

Nov 7

TImp.v

TImp.v

QC

Nov 12

MoreStlc.v ,References.v

Project Proposals Due

PLF

Nov 14

System F

PLF

Nov 19

Normalization of STLC

OPLSS Lecture Notes

PLF

Nov 21

Fun with Dependent Types

Certified Programming with Dependent Types

CPDT

Nov 26/28

Thanksgiving!

PLF

Dec 3

Project Presentations

Dec 5

Project Presentations

Dec 16

Final Projects Due

PLF