I'm looking for verified textbook algorithms in Coq. Do you have some pointers to the latest developments and verification frameworks? I'm aware of CFML and e.g. their work on Union-Find (and an incremental cycle detection algorithm). Further, Pottier's work, e.g. verification of an SCC algorithm. And many more basic algorithms and tree data structures. I'd be happy for some pointers.

[edit] ah, I guess I misunderstood textbook here. For example, incremental cycle detection is not "textbook" in my world. I believe Boldo and Melquiond's book has quite a few textbook floating-point algorithms verified (some of which live in Flocq library, etc.)

I guess you are right about incremental cycle detection, I put it into brackets; but union-find and SCC I'd consider "textbook".

you should probably take a look in https://github.com/coq-contribs and https://github.com/coq-community if anything is textbook enough. For example, I would count Huffman coding and Buchberger's algorithm as textbook (coq-community)

I think many translations here are also "standard" (e.g., DFA minimization): https://github.com/coq-community/reglang

but for precision, is this for some inter-proof-assistant comparison?

rather for collecting what "standard" algorithms were verified in the ITP community. thanks for your pointers!

you can see a list of some (program) verification frameworks in Coq here: https://github.com/coq-community/awesome-coq#frameworks - pretty sure both Iris and VST has many textbook algorithms verified, but they might not be available as separate projects. FCSL verified many textbook concurrent algorithms (http://software.imdea.org/fcsl/)

many Coq algorithm formalizations are mentioned as sidenotes in papers, so you probably want to search the usual databases for "Coq textbook algorithm" and the like, e.g., I saw that the AKS prime algorithm (textbook at this point in my mind) was done in 2008: http://flaviomoura.info/files/sbmf08.pdf

Following your last remark I came across Hing Lun Chan's PhD thesis verifying AKS and its running time in HOL4.

ah, but then you get into the long PL-vs.-complexity debate how running time is even formalized. Coq has a library of Turing machines and the like which may eventually have something fundamental on what O(1) actually means: https://github.com/uds-psl/coq-library-undecidability

one example in Coq of the formalization of "ad-hoc" running time is for the average-case complexity of QuickSort: https://github.com/coq-contribs/quicksort-complexity

I don't know if you're looking for cutting edge or pointer-y stuff, but volume 3 of software foundations is a good source of textbook algorithms https://softwarefoundations.cis.upenn.edu/vfa-current/index.html

Last updated: Aug 03 2024 at 00:02 UTC