Verifying the correctness of a paper in the field of algorithms
If a research paper states that a certain theorem is true, can we then
trust this? Anecdotal evidence suggests that, in the field of
programming languages, it is quite common with mistakes in published
research. Sometimes these mistakes are easy to fix, sometimes not.
However, in cases where the research is accompanied by machine-checked
proofs it should (ideally) be easier to trust it. Such machine-checked
proofs are nowadays relatively common—but by no means ubiquitous—in
In the field of algorithms the situation is (as far as I know)
different: machine-checked proofs are rare. However, this does not
necessarily mean that published research in this area contains more
mistakes. Perhaps the research culture is different, with more
complete proofs in papers, and more diligent reviewers. Perhaps it is
also harder to produce machine-checked proofs in this area with
current technology. I do not know.
The aim of this project is to start filling in the gaps in our
knowledge by performing a case study: verifying (or attempting to
verify) a research paper (or parts of it) from the field of algorithms
by using a proof assistant.
Chien-Chung Huang, who used to work here, suggested that the paper
"Popular Matchings in the Stable Marriage Problem"
(http://doi.org/10.1016/j.ic.2012.10.012) by Huang and Kavitha might
be suitable. This paper is rather self-contained, and is not an old
classic that has been scrutinised carefully by many eyes. However,
other choices of paper can certainly be considered.
Given the open-ended nature of this project it might be a good idea to
start with a warm-up exercise, and use the result of this exercise to
recalibrate the final goals of the project. One could for instance start
by verifying the Gale-Shapley algorithm for the stable marriage problem
The proof assistant Agda is developed in Gothenburg and taught in
courses here, and would be a possible choice for this project. However,
other proof assistants provide more automation and larger libraries, and
may thus be preferable.
Prerequisites: Students attempting this project should have a good
background in algorithms, mathematics and type theory.