Formal Methods Foundation


Only few of the electronic lecture notes are available here, most are on blackbroad. This schedule is tentative and subject to change at any time.

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