
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 1418  no class today  no class today Coq Installation Notes 
Preface; Basics (Basics.v) Introduction; functional programming (numbers, lists); basic proofs 

Sep 2125  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 57  Propositions (Props.v)  Logic (Logic.v)  Lecture (CS 105) or Lab (Friend 009)
Homework 3 due Sunday 

Oct 1216  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 1923  Imperative programs (SfLib.v Imp.v)  Imperative programs  Lecture (CS 105)
Homework 5 due Sunday 

Oct 2629  Imperative Programs; omega tactic (Omega.v)  Informal Proofs  Inclass midterm exam (CS 105)
Takehome midterm due 

Fall Break  
Nov 913  Program Equivalence (Equiv.v)  Program Equivalence  Lab (Friend 009)
Homework 6 due Sunday 

Nov 1620  Hoare Logic (Hoare.v)  Hoare Logic  Lecture (CS 105)
Homework 7 due Sunday 

Nov 2325  Smallstep operational semantics (Smallstep.v)  Smallstep O.S.  (holiday)  
Nov 30  Dec 4  Lambdacalculus (Stlc.v)
Homework 8 due 
Lambdacalculus  Lecture (CS 105)
Homework 9 due Sunday 

Dec 711  More lambdacalculus (MoreStlc.v)  t.b.a.  Lab (Friend 009)
Homework 10 due Sunday 

Dec 1418  Compiler Correctness (Compiler.v)  Coq tips; (Induction.v)
The Big Picture 
Lab, upon request  
Jan 8  Homework 11 due  
Jan 1316  Final Exam: Part 1, Part 2 