▼CMSC631:   Program Analysis and Understanding
    ← prev  up  next → 

4 Schedule

Date

 

Class

 

HW

 

Book

Aug 30

 

Preface.html, Basics.html, Basics.v

 

Basics.v, BasicsTest.v, Makefile, _CoqProject

 

Logical Foundations

Sep 01

 

Induction.html, Induction.v

 

Induction.v, InductionTest.v

 

Logical Foundations

Sep 08

 

Lists.html, Lists.v

 

Lists.v, ListsTest.v

 

Logical Foundations

Sep 13

 

Poly.html, Poly.v

 

Poly.v, PolyTest.v

 

Logical Foundations

Sep 15

 

Tactics.html, Tactics.v

 

Tactics.v, TacticsTest.v

 

Logical Foundations

Sep 20

 

Logic.html, Logic.v

 

Logic.v, LogicTest1.v

 

Logical Foundations

Sep 22

 

Logic.html, Logic.v

 

Logic.v, LogicTest1.v

 

Logical Foundations

Sep 27

 

IndProp.html, IndProp.v

 

Logic.v, LogicTest2.v

 

Logical Foundations

Sep 29

 

IndProp.html, IndProp.v

 

IndProp.v, IndPropTest.v

 

Logical Foundations

Oct 04

 

ProofObjects.html, ProofObjects.v

 

ProofObjects.v, ProofObjectsTest.v

 

Logical Foundations

Oct 06

 

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

 

IndPrinciples.v (No HW), Maps.v, MapsTest.v

 

Logical Foundations

Oct 11

 

Imp.html, Imp.v

 

Imp.v, ImpTest.v

 

Logical Foundations

PLF Setup

 

Maps.v, Imp.v, _CoqProject, Makefile

 

Copy these into a new plf directory

 

Programming Language Foundations

Oct 13

 

Auto.html, Auto.v, LtacMagic.v

 

Auto.v

 

Programming Language Foundations

Oct 18

 

Equiv.html, Equiv.v

 

Equiv.v, EquivTest.v

 

Programming Language Foundations

Oct 20

 

Equiv.html, Equiv.v

 

Equiv.v, EquivTest.v

 

Programming Language Foundations

Oct 25

 

Hoare.html, Hoare.v

 

Hoare.v, HoareTest.v

 

Programming Language Foundations

Oct 27

 

Hoare.html, Hoare.v

 

Study for Midterm

 

Programming Language Foundations

Nov 1

 

Hoare2.html, Hoare2.v

 

Hoare2.v, Hoare2Test.v, Midterm Available

 

Programming Language Foundations

Nov 3

 

Typeclasses.html, Typeclasses.v

 

Typeclasses.v (No HW, just optional exercises)

 

QuickChick

Nov 8

 

Preface.html, Introduction.html, Preface.v, Introduction.v, QC.html, QC.v

 

QC.v (HW, graded manually)

 

QuickChick

Nov 10

 

Smallstep.html, Smallstep.v

 

Smallstep.v, SmallstepTest.v, Project Proposal Due

 

Programming Language Foundations

Nov 15

 

Types.html, Types.v

 

Types.v, TypesTest.v

 

Programming Language Foundations

Nov 17

 

Stlc.html, Stlc.v

 

Stlc.v, StlcTest.v

 

Programming Language Foundations

Nov 22

 

StlcProp.html, StlcProp.v, MoreStlc.html, MoreStlc.v

 

StlcProp.v, StlcPropTest.v

 

Programming Language Foundations

Nov 24

 

No Class

 

 

Nov 29

 

Sub.html, Sub.v

 

Sub.v, SubTest.v

 

Programming Language Foundations

Dec 01

 

References.html, References.v

 

References.v, ReferencesTest.v

 

Programming Language Foundations

Dec 06

 

CLASS CANCELED

 

CLASS CANCELED

 

QuickChick

Dec 08

 

Records.html, Records.v, RecordSub.html, RecordSub.v

 

Records.v, RecordsTest.v, RecordSub.v, RecordSubTest.v

 

Programming Language Foundations

Dec 13

 

A Tour of PL Research

 

 

Dec 14

 

Project Due

 

 

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 Monday (unless there’s a holiday, in which case the due date is Tuesday); please submit via ELMS.

    ← prev  up  next →