|
|
Computer Science 510
|
|
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.
| Date | Tuesday, Thursday | Friday | Homework |
|---|---|---|---|
| Feb 4-8 | Introduction; functional programming (numbers, lists); basic proofs: Coq Installation Notes; Preface; Basics; Induction ( Basics.v, Induction.v) | Lab (Friend 009) | Homework 1 |
| Feb 11-15 | Lists & Polymorphism, More about Coq (Lists.v, Poly.v, MoreCoq.v) | Lab (Friend 009) | Homework 2 |
| Feb 18-22 | Propositions, Logic in Coq (Prop.v, Logic.v); Turing essay | Lab (Friend 009) | Homework 3 |
| Feb 25 - Mar 1 | ML programming language interp.ml; Caml core language, Caml reference Sedgewick Algs 3e, §9.7 | Lab (Friend 009) | Homework 4 |
| Mar 4-8 | Proving correctness of functional programs (SfLib.v, Selection.v, Selection2.v, Sort.v ) | Lab (Friend 009) | Homework 5 |
| Mar 11-15 | Imperative programs ( Imp.v) | Take-home midterm due | |
| Spring Break | |||
| Mar 25-29 | Program Equivalence (Equiv.v) | Lab (Friend 009) | Homework 6 |
| Apr 1-5 | Hoare Logic (Hoare.v, HoareAsLogic.v) | Lab (Friend 009) | Homework 7 |
| Apr 8-12 | Small-step operational semantics (Rel.v, Smallstep.v) Type systems (Types.v) |
Lab (Friend 009) | Homework 8 |
| Apr 15-19 | Satisfiability lectures by Sharad Malik (reading: Boolean Satisfiability Solvers) | Lab (Friend 009) | Dafny Homework |
| Apr 22-26 | Separation Logic (reading: Appel, Program Logics for Certified Compilers, chapters 1-3). | Lab (Friend 009) | Homework 9 |
| Apr 29 - May 3 | Satisfiability modulo theories lectures by Aarti Gupta (reading: Satisfiability Modulo Theories by Barrett et al.) | ||
| May 8 | reading period -- no class -- last homework due | Homework 11 due | |
| May 15 | Due date for final project (if not Stlc.v) | ||