### 3` `Handouts

The materials linked below are local copies of the HTML and Coq files available from the textbook’s Web site. They are slightly different. The textbook site has version 4.0, and the local site is version 4.1 (beta), which contains a few more clarifications and fixes for typos. Since the beta version is under active development, local files may be updated during the term, but there shouldn’t be any substantial differences from the stable version.

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 accurate for the first few weeks at least.

Dates below will be updated as we proceed. There will be no classes in the week of September 19-23, 2016.

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)

Maps, Imp, Equiv, Hoare updated Oct 27.

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)Smallstep, Auto, Types updated Nov 16.

Below this line dates are from 2014 (files are current).

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)