4 Schedule

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. (Solutions)

 

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

 

QC.v, QC.html

 

QuickChick: Property-Based Testing for Coq

Oct 31

 

Smallstep.v,Smallstep.html

 

Programming Language Foundations

Nov 05, 07

 

Types.v,Types.html

 

Programming Language Foundations

Nov 12

 

Project Proposals due! TImp.v,TImp.html

 

QuickChick: Property-Based Testing for Coq

Nov 14

 

Perm.v,Perm.html, Sort.v,Sort.html

 

Verified Functional Algorithms

Nov 19

 

Stlc.v,Stlc.html

 

Programming Language Foundations

Nov 21

 

StlcProp.v,StlcProp.html

 

Programming Language Foundations

Nov 26

 

LtacMagic.v

 

DSSS 17

Dec 3,5

 

Full Version of files (download, put in new dir, then make): Verified Quantum Computing Short Version - for use in class: Qubit.v, Qubit.html, Multiqubit.v, Multiqubit.html, SQIMP.v, SQIMP.html,

 

Verified Quantum Computing

Before every class, the Coq (.v) and HTML versions of the lecture materials will be available above. Students are encouraged to follow along inside, ideally within ProofGeneral. After every class, the files will be updated with additional exposition and exercises. Those are due before class on the following Tuesday; please submit via ELMS.