4 Schedule

Week

 

Class

 

HW

 

Book

Sep 01

 

Preface.html, Basics.v, Basics.html

 

Basics.v, BasicsTest.v, Makefile, _CoqProject

 

Logical Foundations

Sep 03

 

Induction.v, Induction.html

 

Induction.v, InductionTest.v

 

Logical Foundations

Sep 08

 

Lists.v, Lists.html

 

Lists.v, ListsTest.v

 

Logical Foundations

Sep 10

 

Poly.v, Poly.html

 

Poly.v, PolyTest.v

 

Logical Foundations

Sep 15

 

Tactics.v, Tactics.html

 

Tactics.v, TacticsTest.v

 

Logical Foundations

Sep 17

 

Logic.v, Logic.html

 

Logic.v, LogicTest.v

 

Logical Foundations

Sep 22

 

Logic.v, Logic.html

 

Logic.v, LogicTest.v

 

Logical Foundations

Sep 24

 

IndProp.v, IndProp.html

 

IndProp.v, IndPropTest.v

 

Logical Foundations

Sep 29

 

ProofObjects.v, ProofObjects.html, IndPrinciples.v, IndPrinciples.html

 

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

 

Logical Foundations

Oct 01

 

Maps.v, Maps.html, Imp.v, Imp.html

 

Maps.v, MapsTest.v

 

Logical Foundations

Oct 06

 

Imp.v, Imp.html

 

Imp.v, ImpTest.v

 

Logical Foundations

Oct 08

 

Auto.v, LtacMagic.v

 

Auto.v (No homework here)

 

Logical Foundations / DSSS 17

PLF Setup

 

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

 

Copy these into a new plf folder

 

Programming Language Foundations

Oct 13

 

Equiv.v

 

Equiv.v, EquivTest.v

 

Programming Language Foundations

Oct 15

 

Hoare.v

 

Hoare.v, HoareTest.v

 

Programming Language Foundations

Oct 20

 

Hoare2.v

 

Hoare.v, Hoare2.v, Hoare2Test.v

 

Programming Language Foundations

Oct 22

 

Typeclasses.v

 

Typeclasses.v

 

QuickChick

Oct 27

 

Midterm Review

 

 

Oct 29

 

MIDTERM

 

Midterm Solutions

 

Nov 03

 

Elections

 

 

Nov 05

 

QC.v

 

QC.v, Introduction.v, Preface.v

 

QuickChick

Nov 10

 

QuickChickTool.v, stack-compiler/Exp.v, stack-compiler/Stack.v, stack-compiler/Makefile, stack-compiler/_CoqProject

 

No Homework

 

QuickChick

Nov 12

 

Smallstep.v

 

Smallstep.v, SmallstepTest.v

 

Programming Language Foundations

Nov 17

 

STLC

 

Project Proposals DUE!

 

Nov 17

 

Types.v

 

Types.v, TypesTest.v

 

Programming Language Foundations

Nov 17

 

Stlc.v

 

Stlc.v, StlcTest.v

 

Programming Language Foundations

Nov 24

 

MoreStlc.v, StlcProp.v

 

MoreStlc.v, StlcProp.v

 

Programming Language Foundations

Nov 26

 

Happy Thanksgiving!

 

 

Dec 1

 

TImp.v

 

TImp.v

 

QuickChick

Dec 3

 

References.v

 

References.v

 

Programming Language Foundations

Dec 8

 

Sub.v

 

 

Programming Language Foundations

Dec 10

 

Guest Lecture by Zoe Paraskevopoulou

 

Certicoq: Compositional Verification in Practice

 

Programming Language Foundations

Dec 15

 

Recommended Due Date for Projects

 

(Reading Day)

 

Dec 22

 

Absolute Final Due Date for Projects

 

(Last Day of Exams)

 

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 Proof General. 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.