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, HigherOrder 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 lambdacalculus

LEC: untyped arith
Prepare: TAPL chap. 3, 4, 5


may 8

No class

Recruitment day


may 15

Smallstep operational semantics

LEC: Smallstep
Prepare: Smallstep.v


may 22

Typed arith, typed lambdacalculus

LEC: typed arith, typed lambdacalculus
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

