Week

Topic

Book

Aug 27

Preface, and Basics.v, Basics.html

Logical Foundations

Aug 29

Induction.v,Induction.html

Logical Foundations

Sep 03

Lists.v,Lists.html, ListsTest.v

Logical Foundations

Sep 05

Poly.v,Poly.html, PolyTest.v

Logical Foundations

Sep 10, 12

Tactics.v,Tactics.html, TacticsTest.v

Logical Foundations

Sep 17,19

Logic.v,Logic.html, LogicTest.v

Logical Foundations

Sep 24

IndProp.v,IndProp.html, IndPropTest.v

Logical Foundations

Sep 26

Maps.v,Maps.html, MapsTest.v

Logical Foundations

Oct 01

Imp.v,Imp.html, ImpTest.v

Logical Foundations

Oct 03

Auto.v,Auto.html

Logical Foundations

Optional

Preface.html, Equiv.v,Equiv.html, plf.zip, Instructions for building PLF

Programming Language Foundations

Oct 10

Homework Files (due Oct 22, Hoare2 does not contain mandatory homework): Hoare.v,Hoare.html, Hoare2.v,Hoare2.html

Programming Language Foundations

Oct 15

Midterm.

Oct 17

Preface.v,Introduction.v, Typeclasses.v,Typeclasses.html

QuickChick: Property-Based Testing for Coq

Oct 22

Guest lecture by Robert Rand: ProofObjects.v, ProofObjectsTest.v, ProofObjects.html

Logical Foundations

Oct 24

Guest lecture by Robert Rand: IndPrinciples.v, IndPrinciplesTest.v, IndPrinciples.html

Logical Foundations

Oct 29

Advanced Random Testing with QuickCheck

QuickChick: Property-Based Testing for Coq

Nov 05

Smallstep and Types and STLC STLCProp

Programming Language Foundations

Nov 12

Project Proposals due! Sub

PLF and LF

Nov - Dec

Advanced Random Testing and Fuzzing, Quantum Verification, Checked C, etc.

Topics in Programming Languages