I'll fill this out more in the future.
For fun, I thought it would be cool to pull together a playgoround of well-known algorithms, and try mechanizing and formalizing them. So far, this contains the following:
- A functional implementation of the Insertion Sort algorithm, along with ~215 lines of Coq formalizing and proving its correctness.