|
|
Computer Science 441
|
|
This schedule is approximate and subject to adjustment.
Be sure to recheck the schedule each Thursday to see
whether Friday's class is a Lecture or Lab.
Lab sessions are at 10:00 and 11:00.
| Date | Monday | Wednesday | Friday | |
|---|---|---|---|---|
| Sep 14-18 | no class today | no class today Coq Installation Notes |
Preface; Basics (Basics.v) Introduction; functional programming (numbers, lists); basic proofs |
|
| Sep 21-25 | Basics; Lists | Lists (Lists.v)
Homework 0 due |
Lab (Friend 009)
Homework 1 due Sunday |
|
| Sep 28 - Oct 2 | Polymorphism (Poly.v) | Polymorphism | Lab (Friend 009)
Homework 2 due Sunday |
|
| Oct 5-7 | Propositions (Props.v) | Logic (Logic.v) | Lecture (CS 105) or Lab (Friend 009)
Homework 3 due Sunday |
|
| Oct 12-16 | ML programming language interp.ml; Caml core language |
ML; Binomial Queues Caml reference Sedgewick Algs 3e, §9.7 |
Lab (Friend 009)
Homework 4 due Sunday |
|
| Oct 19-23 | Imperative programs (SfLib.v Imp.v) | Imperative programs | Lecture (CS 105)
Homework 5 due Sunday |
|
| Oct 26-29 | Imperative Programs; omega tactic (Omega.v) | Informal Proofs | In-class midterm exam (CS 105)
Take-home midterm due |
|
| Fall Break | ||||
| Nov 9-13 | Program Equivalence (Equiv.v) | Program Equivalence | Lab (Friend 009)
Homework 6 due Sunday |
|
| Nov 16-20 | Hoare Logic (Hoare.v) | Hoare Logic | Lecture (CS 105)
Homework 7 due Sunday |
|
| Nov 23-25 | Small-step operational semantics (Smallstep.v) | Small-step O.S. | (holiday) | |
| Nov 30 - Dec 4 | Lambda-calculus (Stlc.v)
Homework 8 due |
Lambda-calculus | Lecture (CS 105)
Homework 9 due Sunday |
|
| Dec 7-11 | More lambda-calculus (MoreStlc.v) | t.b.a. | Lab (Friend 009)
Homework 10 due Sunday |
|
| Dec 14-18 | Compiler Correctness (Compiler.v) | Coq tips; (Induction.v)
The Big Picture |
Lab, upon request | |
| Jan 8 | Homework 11 due | |||
| Jan 13-16 | Final Exam: Part 1, Part 2 | |||