3 Handouts

The materials linked below are local copies of the HTML and Coq files that make up the textbook. Please note that the textbook’s official Web site contains a stable version frozen in late August. We will be working from more recent versions in progress, which contain significant changes made after the freeze. For this course, the official textbook site is not definitive.

For the 2018 offering: Classes for October 9 and 10 will be held on October 11 and 12, respectively, because of rescheduling around the Fall Break. There will be no classes on October 23 and 24.

• Chapter dependencies chart for Vol I, Logical Foundations.

• Sep. 11,12,18: Introduction; reasoning about simple functional programs. (Preface) (Basics) (Basics.v)

• Sep. 18,19: Inductive definitions and proofs. (Induction) (Induction.v) (_CoqProject)

• Sep. 19, 25: Lists and other structured data. (Lists) (Lists.v)

• Sep. 26: Polymorphism and higher-order functions. (Poly) (Poly.v)

• Oct. 2, 3: More essential Coq tactics. (Tactics) (Tactics.v)

• Oct. 3, 11, 12, 16: Logical connectives. (Logic) (Logic.v)

• Oct. 16, 17, 30, 31: Inductive propositions. (IndProp) (IndProp.v)

• Oct. 31: Proof objects. (ProofObjects) (ProofObjects.v)

• Oct. 31: Induction principles. (IndPrinciples) (IndPrinciples.v)

• Oct 31, Nov. 6: Maps. (Maps) (Maps.v)

• Nov. 6,7: Simple imperative programs. (Imp) (Imp.v)
  

• Additional files: (ImpCEvalFun) (ImpCEvalFun.v) (ImpParser) (ImpParser.v)

• Nov. 13: Automation (end of Vol I). (Auto) (Auto.v)
  Additional files: (Postscript) (Bib)

• Chapter dependencies chart for Vol II, Programming Language Foundations. Please note the additional logistics in handling subsequent files as detailed on the assignments Web page.

• Nov. 13, 14: Program equivalence. (Preface) (Equiv) (Equiv.v) (_CoqProject)

• Nov. 20, 21: Hoare logic. (Hoare) (Hoare.v)
  Additional optional files: (Hoare2) (Hoare2.v) (HoareAsLogic) (HoareAsLogic.v)

• Nov. 21, 27: Small-step operational semantics. (Smallstep) (Smallstep.v)

• Nov. 27: Types. (Types) (Types.v)

• Nov. 28: The simply-typed lambda calculus. (Stlc) (Stlc.v)

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

• Items below this point have timings based on the 2016 offering, and files, if available, are not guaranteed to be those used in lecture; that is, they may be updated before moving above this bullet item.

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

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