VFA: Verified Functional Algorithms

• Introduction
• Prerequisites and practicalities
  • Chapter Dependencies
  • System Requirements
  • Exercises
  • Downloading the Coq Files
  • Acknowledgment
  • For instructors and contributors

Perm: Basic techniques for permutations and ordering

• The less-than order on the natural numbers
  • Relating Prop to bool
  • Some advanced tactical hacking.
  • Inversion/clear/subst
  • Linear integer inequalities
• Permutations
• Summary: Comparisons and permutations

Sort: Insertion sort

• Recommended reading
• The insertion-sort program
• Specification of correctness
• Proof of correctness
• Making sure the specification is right
• Proving correctness from the alternate spec
  • The moral of this story

Multiset: Insertion sort with multisets

• Correctness
• Permutations and multisets
• The main theorem: equivalence of multisets and permutations

Selection: Selection sort, with specification and proof of correctness

• The selection-sort program
• Proof of correctness of selection sort.
• Recursive functions that are not structurally recursive

SearchTree: Binary search trees

• Sections
• Program for Binary Search Trees
• Search tree examples
• What should we prove about search trees?
• Efficiency of search trees
• Proof of correctness
  • Relating the operations
• Correctness proof of the elements function.
• Representation invariants
  • Auxiliary lemmas about In and list2map
• Preservation of representation invariant
• We got lucky.
• Every well-formed tree does actually relate to an abstraction
• It wasn't really luck, actually
  • Coherence with elements instead of lookup
• Summary: Abstract Data Types

ADT: Abstract data types

• • A brief excursion into dependent types
  • End of the brief excursion into dependent types
• Summary of Abstract Data Type proofs:
• Exercise in Data Abstraction

Extraction: Running Coq programs in ML

• Utilities for Ocaml integer comparisons.
• SearchTrees, extracted
  • Maps, on Z instead of nat.
  • Trees, on int instead of nat.
• Performance tests
• Unbalanced binary search trees
• Balanced binary search trees

Redblack: Implementation and proof of red-black trees

• Required reading:
• Proof automation for case-analysis proofs.
• The SearchTree property
• Proving efficiency.
• Extracting and measuring red-black trees
• Success!

Trie: Number representations and efficient lookup tables

• logN penalties in functional programming
• A simple program that's waaay too slow.
• Efficient positive numbers
  • Coq's integer type, Z
  • From N*N*N to N*N*logN
  • From N*N*logN to N*logN*logN
• Tries: efficient lookup tables on positive binary numbers
  • From N*logN*logN to N*logN
• Proving the correctness of trie tables
  • Lemmas about the relation between lookup and insert
  • Bijection between positive and nat.
  • Proving that tries are a "table" ADT.
  • Sanity check
• Conclusion

Priqueue: Priority queues

• Module Signature
• Implementation
  • Some preliminaries
  • The program
• Predicates on priority queues
  • The representation invariant
  • Sanity checks on the Abstraction relation
  • Characterizations of the operations on queues

Binom: Binomial queues

• • Required reading
• The program
• Characterization predicates
• Proof of algorithm correctness
  • Various functions preserve the representation invariant
  • The abstraction relation
  • Sanity checks on the abstraction relation
  • Various functions preserve the abstraction relation
  • Optional exercises
• Measurement.

Decide: programming with decision procedures

• Using reflect to characterize decision procedures
• Using sumbool to characterize decision procedures
  • sumbool in the Coq standard library
• Decidability and computability
• Opacity of Qed
• Advantages and disadvantages of reflect versus sumbool

Color: Graph coloring

• Preliminaries: Representing graphs
• Lemmas about sets and maps
  • equivlistA
  • SortA_equivlistA_eqlistA
  • S.remove and S.elements
  • Lists of (key,value) pairs
  • Cardinality
• Now begins the graph coloring program
  • Some proofs in support of termination
  • The rest of the algorithm
• Proof of correctness of the algorithm.
• Trying out the algorithm on an actual test case