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.