| Date |
Topic |
Lectures |
Assignments |
|
feb. 20
|
Introduction
|
LEC: introduction
(Preface.v)
Prepare: software setup
|
Finish Basics.v
|
|
feb. 27
|
Functional programming
|
LEC: Basics
Prepare: Basics.v
|
Finish Induction.v
|
|
mar. 6
|
Induction
|
LEC: Induction
Prepare: Induction.v
|
Finish Lists.v
|
|
mar. 13
|
Lists
|
LEC: Lists
Prepare: Lists.v
|
Finish Poly.v
|
|
mar. 20
|
Polymorphism, Higher-Order Functions
More Coq
|
LEC: Poly
LEC: More Coq
Prepare: Poly.v
Prepare: MoreCoq.v
Read: MapReduce
|
Finish Prop.v
|
|
march. 27
|
Propositions and Evidence
More Prop
|
LEC: Prop
LEC: MoreProp
Prepare: Prop.v
Prepare: MoreProp.v
|
Finish Logic.v
|
|
apr. 3
|
Logic
|
LEC: Logic
Prepare: Logic.v
Read: chap 2 of
CMU notes
Read: From Frege to Gosling
|
Finish ProofObjects.v
|
|
apr. 10
|
Midterm test I
|
|
|
|
apr. 17
|
Proof Objects
|
LEC: ProofObjects
Prepare: ProofObjects.v
|
Finish MoreInd.v
|
|
apr. 24
|
More on Induction
|
LEC: MoreInd
Prepare: Imp.v
|
Finish Imp.v
|
|
may 1
|
Untyped arith, untyped lambda-calculus
|
LEC: untyped arith
Prepare: TAPL chap. 3, 4, 5
|
|
|
may 8
|
No class
|
Recruitment day
|
|
|
may 15
|
Small-step operational semantics
|
LEC: Smallstep
Prepare: Smallstep.v
|
|
|
may 22
|
Typed arith, typed lambda-calculus
|
LEC: typed arith, typed lambda-calculus
Prepare: TAPL chap. 8, 11
|
|
|
may 29
|
Types in Coq
|
LEC: Types, Stlc
Prepare: Types, Stlc
|
|
|
june 5
|
Midterm test II
|
Close book, close notes, no electronic devices
|
|
|
june 12
|
MoreStlc
|
LEC: More Stlc
Prepare: More Stlc
|
|
|
june 19
|
Program Equivalence
|
LEC: Equiv
Prepare: Equiv.v
|
|
|
june 26
|
Hoare logic
|
LEC: Hoare
Prepare: Hoare.v
|
|
|
july 3
|
Subtyping
|
LEC: Sub
Prepare: Sub.v
|
|
|
july 10
|
Final test
|
Close book, close notes, no electronic devices
|
|