TODOs

[simnalamburt]

1. Vol 1, Logical Foundations

   • Preface
   • Functional Programming in Coq (Basics)
     • Initial pass complete, needs review.
   • Proof by Induction (Induction)
     • Initial pass complete, needs review.
   • Working with Structured Data (Lists)
     • Initial pass complete, needs review.
   • Polymorphism and Higher-Order Functions (Poly)
   • More Basic Tactics (Tactics)
   • Logic in Coq (Logic)
   • Inductively Defined Propositions (IndProp)
   • Total and Partial Maps (Maps)
   • ProofObjects
   • Induction Principles (IndPrinciples)
   • Properties of Relations (Rel)
   • Simple Imperative Programs (Imp)
   • Lexing and Parsing in Coq (ImpParser)
   • An Evaluation Function for Imp (ImpCEvalFun)
   • Extracting OCaml from Rocq (Extraction)
   • More Automation (Auto)
   • A Streamlined Treatment of Automation (AltAuto)
   • Postscript
   • Bibliography (Bib)

2. Vol 2, Programming Language Foundations

   • Preface
   • Program Equivalence (Equiv)
   • Hoare Logic, Part I (Hoare)
   • Hoare Logic, Part II (Hoare2)
   • Hoare Logic as a Logic (HoareAsLogic)
   • Small-step Operational Semantics (Smallstep)
   • Type Systems (Types)
   • The Simply Typed Lambda-Calculus (Stlc)
   • Properties of STLC (StlcProp)
   • More on the Simply Typed Lambda-Calculus (MoreStlc)
   • Subtyping (Sub)
   • A Typechecker for STLC (Typechecking)
   • Adding Records to STLC (Records)
   • Typing Mutable References (References)
   • Subtyping with Records (RecordSub)
   • Normalization of STLC (Norm)
   • Partial Evaluation (PE)
   • Postscript
   • Bibliography (Bib)
   • A Collection of Handy General-Purpose Tactics (LibTactics)
   • Tactic Library for Coq: A Gentle Introduction (UseTactics)
   • Theory and Practice of Automation in Coq Proofs (UseAuto)

3. Vol 3, Verified Functional Algorithms

   • Preface
   • Basic Techniques for Comparisons and Permutations (Perm)
   • Insertion Sort (Sort)
   • Insertion Sort Verified With Multisets (Multiset)
   • Insertion Sort With Bags (BagPerm)
   • Selection Sort (Selection)
   • Merge Sort, With Specification and Proof of Correctness (Merge)
   • Total and Partial Maps (Maps)
   • Binary Search Trees (SearchTree)
   • Abstract Data Types (ADT)
   • Running Coq Programs in OCaml (Extract)
   • Red-Black Trees (Redblack)
   • Number Representations and Efficient Lookup Tables (Trie)
   • Priority Queues (Priqueue)
   • Binomial Queues (Binom)
   • Programming with Decision Procedures (Decide)
   • Graph Coloring (Color)

4. Vol 4, QuickChick: Property-Based Testing in Coq

   • Preface
   • Introduction
   • A Tutorial on Typeclasses in Coq (Typeclasses)
   • Core QuickChick (QC)
   • Case Study: a Typed Imperative Language (TImp)
   • The QuickChick Command-Line Tool (QuickChickTool)
   • QuickChick Reference Manual (QuickChickInterface)
   • Postscript
   • Bibliography (Bib)

5. Vol 5, Verifiable C

   • Preface
   • Introduction to Verifiable C (Verif_sumarray)
   • Linked lists in Verifiable C (Verif_reverse)
   • Stack ADT implemented by linked lists (Verif_stack)
   • A client of the stack functions (Verif_triang)
   • List segments (Verif_append1)
   • Magic wand, partial data structure (Verif_append2)
   • String functions (Verif_strlib)
   • Functional model of hash tables (Hashfun)
   • Correctness proof of hash.c (Verif_hash)
   • Introduction to Verified Software Units (VSU_intro)
   • VSU specification of the Stack module (Spec_stack)
   • VSU specification of the Triang module (Spec_triang)
   • Specification of external malloc, free, exit functions (Spec_stdlib)
   • VSU verification of the Stack module (VSU_stack)
   • VSU verification of the Triang module (VSU_triang)
   • Axiomatization of malloc/free/exit (VSU_stdlib)
   • linking all the VSUs together with main VSU (VSU_main)
   • Malloc/free/exit programmed in C (VSU_stdlib2)
   • linking with stdlib2 instead of with stdlib (VSU_main2)
   • Postcript and bibliography (Postscript)
   • Bibliography (Bib)

6. Vol 6, Separation Logic Foundations

   • Introduction to the Course (Preface)
   • Basic Proofs in Separation Logic (Basic)
   • Representation Predicates (Repr)
   • Heap Predicates (Hprop)
   • Heap Entailment (Himpl)
   • Structural Reasoning Rules (Triples)
   • Reasoning Rules for Term Constructs (Rules)
   • The Magic Wand and Other Operators (Wand)
   • Semantics of Weakest Preconditions (WPsem)
   • Weakest Precondition Generator (WPgen)
   • Soundness of the Weakest Precondition Generator (WPsound)
   • Affine Separation Logic (Affine)
   • Reasoning about Arrays (Arrays)
   • Reasoning about Records (Records)
   • Conclusion and Perspectives (Postscript)
   • Bibliography (Bib)
   • Appendix - The Full Construction (LibSepReference)
   • Appendix - Finite Maps (LibSepFmap)
   • Appendix - Program Variables (LibSepVar)
   • Appendix - Simplification Tactic for Entailments (LibSepSimpl)
   • Appendix - Minimalistic Soundness Proof (LibSepMinimal)