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

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)