| Date |
Monday, Wednesday |
Thu/Fri |
Homework |
| Feb 1-5 |
Introduction; functional programming (numbers, lists); basic proofs:
Coq Installation Notes;
Preface; Basics; Induction; Lists (
Basics.v,
Induction.v,
Lists.v
) |
Lab |
Homework 1 |
| Feb 8-12 |
Sequent Calculus,
Polymorphism, More basic tactics (Poly.v, Tactics.v) |
Lab |
Homework 2 |
| Feb 15-19 |
Logic in Coq,
Inductively defined propositions,
Curry-Howard correspondence
(Logic.v, IndProp.v,
ProofObjects.v) |
Lab |
Homework 3 |
| Feb 22-26 |
ML programming language;
Caml core language, Caml reference;
Ocaml+Emacs;
interp.ml, lambda.ml;
Denotational Semantics;
Binomial Queues,
Maps
| Lab |
Homework 4 |
| Mar 1-5 |
Proving correctness of functional programs,
permutations,
selection sort,
insertion sort
(VFA.v,
Perm.v,
Selection.v,
Sort.v)
Maps,
Search Trees,
Abstract Data Types
(Maps.v
SearchTree.v,
ADT.v)
|
Lab |
Homework 5 |
| Mar 8-12 |
SOS, Imperative programs,
Automation
( Imp.v, Auto.v);
Search trees,
Red-Black trees,
(SearchTree.v,
Redblack.v)
|
Take-home midterm due |
| Spring Break: No class March 17
|
| Mar 22-26 |
Program Equivalence (Equiv.v), Hoare Logic (Hoare.v) |
Lab |
Homework 6 |
| Mar 29-Apr 2 |
Hoare Logic (Hoare2.v),
Small-step operational semantics (Smallstep.v),
Type systems
(lecture notes; Types.v)
|
Lab |
Homework 7 |
| Apr 5-9 |
Simply typed lambda calculus;
Type Soundness;
subtyping
(lecture notes,
Stlc.v, StlcProp.v, Sub.v)
|
Lab |
Homework 8 |
| Apr 12-16 |
SAT, SMT (reading: Boolean Satisfiability Solvers); Dafny (selection sort)
|
Lab |
Homework 9
|
| Apr 19-23 |
Separation Logic
(read Chapters 2 and 3 of PLCC); Verifiable C, vc.tgz
|
Lab |
|
| Apr 26-28 |
Verifying C programs (Verifiable C),
vc.tgz
|
Lab |
|
| Apr 28 |
reading period: there will be class on April 28, see line above. |
|
| May 4 |
Homework 10 due (if you're not doing Homework 11) |
Homework 10 |
| May 10 |
Homework 11 due (if you didn't do Homework 10) |
Homework 11
|
