### 3` `Handouts

The materials linked below are local copies of the HTML and Coq files available from the textbook’s Web site. They may be slightly different.

Timings below are approximate and will be changed as the term progresses. The initial schedule is based on the previous offering, and the textbook has been revised since then, but it should be roughly accurate for the first few weeks at least.

Dates below are from earlier offerings, and will be updated as we proceed. There will be no classes in the week of October 22-26, 2018.

Sep. 14: Introduction; reasoning about simple functional programs. (Preface) (Basics) (Basics.v)

Sep. 28, Oct. 5: Inductive definitions and proofs. (Induction) (Induction.v)

Oct. 5: Polymorphism and higher-order functions. (Poly) (Poly.v)

Oct. 5, 12: More essential Coq tactics. (Tactics) (Tactics.v)

Oct. 26: Proof objects. (ProofObjects) (ProofObjects.v)

Oct. 26: Induction principles. (IndPrinciples) (IndPrinciples.v)

Nov. 2: Simple Imperative Programs. (Imp) (Imp.v)

Additional files: (ImpCEvalFun) (ImpCEvalFun.v) (ImpParser) (ImpParser.v)Nov. 16: Hoare logic. (Hoare) (Hoare.v)

Additional optional files: (Hoare2) (Hoare2.v) (HoareAsLogic) (HoareAsLogic.v)Nov. 6, 11: Small-step operational semantics. (Smallstep) (Smallstep.v)

Nov. 20: Properties of the simply-typed lambda calculus. (StlcProp) (StlcProp.v)

If time: Extending the simply-typed lambda calculus. (MoreStlc) (MoreStlc.v)

If time: Typechecking. (Typechecking) (Typechecking.v)