|
Computer Science 441
|
|
This schedule is approximate and subject to adjustment. Recheck the schedule each Thursday to see whether Friday's class is a Lecture or Lab. Friday Lab sessions are two hours, 10:00-11:50, and you can arrive late or leave early. Lectures are at 10:00 and I would appreciate it if you arrive on time.
Sunday Labs are entirely optional: you can get assistance with the homeworks Sundays 5-7 pm and 8:30-10:30 pm in Friend 009 (or Friend 007 or 005 if for some reason 009 is occupied by a special event).
| Date | Monday, Wednesday | Friday | Sunday |
|---|---|---|---|
| Sep 13-19 | classes start Friday Coq Installation Notes |
Preface; Basics (Basics.v) Introduction; functional programming (numbers, lists); basic proofs |
Homework 0 due next Tuesday |
| Sep 20-26 | Basics; Lists (Lists.v) | Lab (Friend 009) | Homework 1 |
| Sep 27 - Oct 3 | Polymorphism (Poly.v) | Lab (Friend 009) | Homework 2 |
| Oct 4-10 | Propositions (Ind.v) | Lab (Friend 009) | Homework 3 |
| Oct 11-17 | Logic (Logic.v, Rel.v) | Lab (Friend 009) | Homework 4 |
| Oct 18-24 | ML programming language interp.ml; Caml core language, Caml reference Sedgewick Algs 3e, §9.7 |
Lab (Friend 009) | Homework 5 |
| Oct 25-30 | Proving correctness of functional programs | In-class midterm exam (CS 105! NOTE DIFFERENT ROOM)
Take-home midterm due |
|
| Fall Break | |||
| Nov 8-14 | Imperative programs (SfLib.v Imp.v) | Lecture (CS 102) | Homework 6 |
| Nov 15-21 | Program Equivalence (Equiv.v) | Lab (Friend 009) | Homework 7 |
| Nov 22-28 | Hoare Logic (Hoare.v) | (holiday) | Homework 8 due Monday |
| Nov 29 - Dec 5 | Mon: Lab; Weds, Fri: Small-step operational semantics (Smallstep.v) | Homework 9 | |
| Dec 6-12 | Lambda-calculus (Stlc.v) | Lab (Friend 009) | Homework 10 |
| Dec 13-17 | More lambda-calculus (MoreStlc.v) | Lab, upon request | |
| Jan 10 | Homework 11 due | ||
| Jan 12-15 | Final Exam | ||