Week

Class

HW

Book

Aug 29

Preface.v, Basics.v, _CoqProject

Basics.v, BasicsTest.v, Makefile

Logical Foundations

Aug 31

Induction.v, Lists.v

Induction.v, InductionTest.v

Logical Foundations

Sep 05

Poly.v, Tactics.v

Lists.v (no HW), Poly.v, PolyTest.v, Tactics.v, TacticsTest.v

Logical Foundations

Sep 08

ICFP

Logical Foundations

Sep 12

Logic.v

Logic.v, LogicTest.v

Logical Foundations

Sep 14

IndProp.v

IndProp.v, IndPropTest.v

Logical Foundations

Sep 19

ProofObjects.v, IndPrinciples.v

ProofObjects.v, ProofObjectsTest.v, IndPrinciples.v

Logical Foundations

Sep 21

Maps.v, Imp.v

Maps.v, MapsTest.v

Logical Foundations

Sep 26

Continue Imp, Auto.v

Imp.v, ImpTest.v, Auto.v

Logical Foundations

PLF Setup

Maps.v, Imp.v, _CoqProject.v,Makefile

Copy these into a new plf folder

Programming Language Foundations

Sep 28

Equiv.v

Equiv.v, EquivTest.v

Programming Language Foundations

Oct 03

Hoare.v

Hoare.v, HoareTest.v

Programming Language Foundations

Oct 05

Hoare2.v

Hoare2.v

Programming Language Foundations

Oct 10

Smallstep.v

Smallstep.v, SmallstepTest.v

Programming Language Foundations

Oct 12

Types.v

Types.v, TypesTest.v

Programming Language Foundations

Oct 17

Preface.v, Introduction.v, Makefile, _CoqProject, Typeclasses.v

QuickChick

Oct 19

Midterm Review

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

QuickChick

Oct 24

MIDTERM

Oct 26

Stlc.v

Stlc.v,StlcTest.v

PLF

Oct 31

StlcProp.v, MoreStlc.v

StlcProp.v, StlcPropTest.v

PLF

Nov 2

Class Cancelled - Illness

Nov 7

QC.v

QC

Nov 9

TImp.v

QC

Nov 14

Project Proposals Due

Nov 14

References.v

PLF

Nov 16

Normalization (Whiteboard)

OPLSS Lecture Notes

Nov 21/23

Thanksgiving!

PLF

Nov 28

System F

PLF

Nov 30

Type Inference

PLF

Dec 5

Project Presentations

Lana: 10’. Guido: 5’. Austin: 5’. Will: 5’. Ethan: 5’. Nikhil: 10’. Anushka: 15’.

Dec 7

Project Presentations

Dec 16

Final Projects Due

PLF