Jan 30  Feb 3 
Introduction; functional programming (numbers, lists); basic proofs:
Coq Installation Notes;
Preface; Basics; Induction; Lists (
Basics.v,
Induction.v,
Lists.v
) 
Lab 
Homework 1 
Feb 610 
Sequent Calculus,
Polymorphism, More basic tactics (Poly.v, Tactics.v) 
Lab 
Homework 2 
Feb 1317 
Logic in Coq,
Inductively defined propositions,
CurryHoward correspondence
(Logic.v, IndProp.v,
ProofObjects.v) 
Lab 
Homework 3 
Feb 2024 
ML programming language;
Caml core language, Caml reference;
Installing Ocaml;
interp.ml, lambda.ml;
Denotational Semantics;
Binomial Queues,
Maps
 Lab 
Homework 4 
Feb 27  Mar 3 
Proving correctness of functional programs,
permutations,
selection sort,
insertion sort
(VFA.v,
Perm.v,
Selection.v,
Sort.v)
Maps,
Search Trees,
Abstract Data Types
(Maps.v
SearchTree.v,
ADT.v)

Lab 
Homework 5 
Mar 610 
SOS, Imperative programs,
Automation
( Imp.v, Auto.v);
Search trees,
RedBlack trees,
(SearchTree.v,
Redblack.v),
BentleySedgewick Trees

Takehome midterm due 
Spring Break: No class March 1317

Mar 2024 
Program Equivalence (Equiv.v), Hoare Logic (Hoare.v) 
Lab 
Homework 6 
Mar 2731 
Hoare Logic (Hoare2.v),
Smallstep operational semantics (Smallstep.v),
Type systems
(lecture notes; Types.v)

Lab 
Homework 7 
Apr 37 
Simply typed lambda calculus;
Type Soundness;
subtyping
(lecture notes,
Stlc.v, StlcProp.v, Sub.v)

Lab 
Homework 8 
Apr 1014 
SAT, SMT (reading: Boolean Satisfiability Solvers); Dafny (selection sort)

Lab 
Homework 9

Apr 1721 
Separation Logic
(read Chapters 2 and 3 of PLCC); Verifiable C, vc.tgz

Lab 

Apr 2428 
Verifying C programs (Verifiable C),
vc.tgz

Lab 

May 1 
Reading period 

May 9 
Homework 10 due (if you're not doing Homework 11) 
Homework 10 
May 12 
Homework 11 due (if you didn't do Homework 10) 
Homework 11
