Basically, trying to verify some data structures/functional algorithms
in Coq/SSReflect, using dependent types, and using Program whenever it makes sense
(unlike most Coq hackers). Currently, mostly formalizing tree structures. Those
are the algorithms/data structures I have formalized/am formalizing:
- Sorted lists: vds_sort.v
- Quicksort: quicksort.v
- Red-black trees (with ML types): red_black.v
- 2-3 trees (with dependent types); deletion is hard and still in progress: twothree_dependent.v and twothree_dependent_delete.v
Xuanrui (Ray) Qi. Email: me@xuanruiqi.com.
All of my code is released into the public domain.