Week

Class

HW

Book

Aug 29

Preface.v, Basics.v, _CoqProject

Basics.v, BasicsTest.v, Makefile

Logical Foundations

Sep 01

Induction.v, Lists.v

Induction.v, Lists.v, InductionTest.v, ListsTest.v

Logical Foundations

Sep 06

Poly.v, Tactics.v

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

Logical Foundations

Sep 08

Logic.v

Logic.v

Logical Foundations

Sep 13

IndProp.v

IndProp.v, IndPropTest.v

Logical Foundations

Sep 15

ProofObjects.v

ProofObjects.v, ProofObjectsTest.v

Logical Foundations

Sep 20

IndPrinciples.v

IndPrinciples.v, IndPrinciplesTest.v

Logical Foundations

Sep 22

Maps.v, Imp.v

Maps.v, MapsTest.v

Logical Foundations

Sep 27

Auto.v

Imp.v, ImpTest.v, Auto.v

Logical Foundations

PLF Setup

Maps.v, Imp.v, _CoqProject.v

Copy these into a new plf folder

Programming Language Foundations

Sep 29

Equiv.v

Equiv.v, EquivTest.v

Programming Language Foundations

Oct 04

Hoare.v

Hoare.v, HoareTest.v

Programming Language Foundations

Oct 06

Hoare2.v

Hoare2.v

Programming Language Foundations

Oct 11

LtacMagic.v

No HW!

Programming Language Foundations

Oct 13

Introduction.v, Typeclasses.v, _CoqProject.v

Install QuickChick!

QuickChick

Oct 18

QC.v

QuickChick

Oct 20

Midterm Review

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

QuickChick

Oct 25

MIDTERM

Oct 27

Smallstep.v

Smallstep.v, SmallstepTest.v

PLF

Nov 1

Types.v

PLF

Nov 3

TImp.v

QC

Nov 8

Stlc.v

PLF

Nov 10

Project Proposals Due

Nov 10

StlcProp.v, MoreStlc.v

PLF

Nov 15

Norm.v

PLF

Nov 17

Records.v

PLF

Nov 22/24

Thanksgiving!

PLF

Nov 29

Sub.v

PLF

Dec 1

References.v

PLF

Dec 6

PLMW Language Quiz

Dec 8

Project Presentations

Dec 12

Final Projects Due

PLF