Date |
Monday, Wednesday |
Friday |
Homework |
Feb 6-10 |
Introduction; functional programming (numbers, lists); basic proofs:
Coq Installation Notes;
Preface; Basics; Induction; Lists (
Basics.v,
Induction.v,
Lists.v
) |
Lab |
Homework 1 |
Feb 13-17 |
Sequent Calculus,
Polymorphism, More basic tactics (Poly.v, Tactics.v) |
Lab |
Homework 2 |
Feb 20-24 |
Logic in Coq,
Inductively defined propositions,
Curry-Howard correspondence,
Maps
(Logic.v, IndProp.v,
ProofObjects.v,
Maps.v) |
Lab |
Homework 3 |
Feb 27-Mar 3 |
ML programming language
interp.ml;
Caml core language, Caml reference
Sedgewick Algs 3e, §9.7
| Lab |
Homework 4 |
Mar 6-10 |
Proving correctness of functional programs,
permutations,
selection sort,
insertion sort
(VFA.v,
Perm.v,
Selection.v,
Sort.v) |
Lab |
Homework 5 |
Mar 13-17 |
Imperative programs ( Imp.v);
Search trees
(SearchTree.v)
|
Take-home midterm due |
Spring Break |
Mar 27-31 |
Program Equivalence (Equiv.v), Hoare Logic (Hoare.v) |
Lab |
Homework 6 |
Apr 3-7 |
Hoare Logic (Hoare2.v),
Small-step operational semantics (Smallstep.v) |
Lab |
Homework 7 |
Apr 10-14 |
Tactic automation
(Auto.v),
red-black trees
(Redblack.v);
Type systems
(lecture notes; Types.v)
|
Lab |
Homework 8 |
Apr 17-21 |
Satisfiability (reading: Boolean Satisfiability Solvers)
|
Lab |
Homework 9
|
Apr 24-30 |
Lambda Calculus
(STLC.pdf,
Stlc.v,
StlcProp.v,
MoreStlc.v,
Typechecking.v);
Birth of CS
| Lab |
Project proposal |
May 1-5 |
extraction;
abstract data types
(Extraction.v,
ADT.v);
Separation Logic
(read Chapters 2 and 3 of PLCC).
|
|
May 8 |
reading period -- no class -- last homework due |
Homework 10 or
Project Checkpoint
due |
May 16 |
Due date for final project (if not Stlc.v) |