Verified functional algorithms Andrew W. Appel

Write your program in an expressive language—Gallina—with a clean and tractable proof theory—CiC—and then prove it correct in Coq. This is a powerful way to produce verified software. Since we want our programs to be efficient, we want to implement sophisticated data structures and algorithms. Since Gallina is a purely functional language, it helps to have purely functional algorithms. In these lectures I show the principles and practice of functional algorithms, and how to verify them in Coq.

Preparation

• Install Coq 8.6.
• Download the tarball of .v files for VFA and make sure they compile, and that you can step through them in the IDE of your choice.
• Read the following to refresh your memory about the basics of insertion sort, selection sort, binary search trees, red-black trees:

  Insertion sort

  Wikipedia (first 45% of that page), or
  Sections 2.0 and 2.1 of Algorithms, Fourth Edition, by Sedgewick and Wayne, Addison Wesley 2011; or
  Section 2.1 of Introduction to Algorithms, 3rd Edition, by Cormen, Leiserson, and Rivest, MIT Press 2009.
  Selection sort
  Wikipedia (first 55% of that page),
  or from Sedgewick and Wayne, or from Cormen, Leiserson, and Rivest.
  Binary search trees
  Wikipedia (first 45% of that page), or
  Section 3.2 of Algorithms, Fourth Edition, by Sedgewick and Wayne, Addison Wesley 2011; or
  Chapter 12 of Introduction to Algorithms, 3rd Edition, by Cormen, Leiserson, and Rivest, MIT Press 2009.
  Red-black trees
  Wikipedia (first 45% of that page), or
  Section 3.3 of Algorithms, Fourth Edition, by Sedgewick and Wayne, Addison Wesley 2011; or
  Chapter 13 of Introduction to Algorithms, 3rd Edition, by Cormen, Leiserson, and Rivest, MIT Press 2009.

Day one: Sorting

Day two: Search Trees

Day three: Search Trees

Day four: Separation Logic

---