maximilian p.l. haslbeck (Jul 08 2020 at 08:33): maximilian p.l. haslbeck (Jul 08 2020 at 08:33):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.
Karl Palmskog (Jul 08 2020 at 08:34):[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.)
maximilian p.l. haslbeck (Jul 08 2020 at 08:38):I guess you are right about incremental cycle detection, I put it into brackets; but union-find and SCC I'd consider "textbook".
Karl Palmskog (Jul 08 2020 at 08:41):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)
Karl Palmskog (Jul 08 2020 at 08:46):I think many translations here are also "standard" (e.g., DFA minimization): https://github.com/coq-community/reglang
Karl Palmskog (Jul 08 2020 at 08:48):but for precision, is this for some inter-proof-assistant comparison?
maximilian p.l. haslbeck (Jul 08 2020 at 08:54):rather for collecting what "standard" algorithms were verified in the ITP community. thanks for your pointers!
Karl Palmskog (Jul 08 2020 at 08:58):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/)
Karl Palmskog (Jul 08 2020 at 09:02):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
maximilian p.l. haslbeck (Jul 08 2020 at 10:16):Following your last remark I came across Hing Lun Chan's PhD thesis verifying AKS and its running time in HOL4.
Karl Palmskog (Jul 08 2020 at 10:19):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
Karl Palmskog (Jul 08 2020 at 10:21):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
Philip Zucker (Jul 11 2020 at 17:32):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: Sep 30 2023 at 15:01 UTC