This schedule is approximate and subject to adjustment.
Friday Lab sessions are two hours, 10:00-11:50, and you can
arrive late or leave early. Lectures are at 11:00 and
I would appreciate it if you arrive on time.
| Date |
Monday, Wednesday |
Friday |
Homework |
| Feb 2-6 |
Introduction; functional programming (numbers, lists); basic proofs:
Coq Installation Notes;
Preface; Basics; Induction; Lists (
Basics.v,
Induction.v,
Lists.v
) |
Lab |
Homework 1 |
| Feb 9-13 |
Sequent Calculus,
Polymorphism, More about Coq (Poly.v, MoreCoq.v) |
Lab |
Homework 2 |
| Feb 16-20 |
Logic in Coq,
Propositions,
MoreLogic
(Logic.v, Prop.v, MoreLogic.v) |
Lab |
Homework 3 |
| Feb 23-7 |
ML programming language
interp.ml;
Caml core language, Caml reference
Sedgewick Algs 3e, §9.7
| Lab |
Homework 4 |
| Mar 2-6 |
Proving correctness of functional programs
(SfLib.v,
Selection.v,
Selection2.v,
Sort.v) |
Lab |
Homework 5 |
| Mar 9-13 |
Imperative programs ( Imp.v) |
Take-home midterm due |
| Spring Break |
| Mar 23-26 |
Program Equivalence (Equiv.v) |
Lab |
Homework 6 |
| Mar 30- Apr 3 |
Hoare Logic (Hoare.v, Hoare2.v, HoareAsLogic.v) |
Lab |
Homework 7 |
| Apr 6-10 |
Small-step operational semantics (Rel.v, Smallstep.v)
Type systems
(Types.v)
|
Lab |
Homework 8 |
| Apr 13-17 |
Satisfiability (reading: Boolean Satisfiability Solvers)
|
Lab |
Homework 9
|
| Apr 20-24 |
Lambda Calculus
(Stlc.v,
StlcProp.v,
Typechecking.v);
Turing essay.
| Lab |
Project proposal |
| Apr 27 - May 1 |
Satisfiability modulo theories
(reading: Satisfiability Modulo Theories by Barrett et al.)
|
|
| May 6 |
reading period -- no class -- last homework due |
Homework 10 or
Project Checkpoint
due |
| May 13 |
Due date for final project (if not Stlc.v) |
