My proposed research topics are of the theme: formalize a theory X, apply to verification of algorithm Y. I still haven’t picked a topic to go ahead. Here are some of my thoughts:
- Turtle Geometry – Differential geometry and topology are the theories behind advanced turtle geometry. This is a wide range of topics – perhaps too many. The algorithms are just graphic procedures, although their validity are based on theorems. Such graphic algorithms probably have no practical applications, so are they worth verifying?
- Fractal Art – Like turtles, graphic algorithms to display fractals probably don’t have research value. Generating fractals is based on the theory of IFS. There is one practical application of IFS: (natural) image compression. I’m not sure if compression algorithms are worth verifying.
- Elliptic Curves – The theory of elliptic curves (EC) overlaps with number theory, group theory and modular forms. There are many elliptic curve algorithms in actual use, including factoring and cryptography. Certainly there are incentives to verify these algorithms, and Joe Hurd had been working on EC cryptography. Will doing only EC factoring be enough for research work?
I was thinking, formalizing EC is just putting textbook math into the theorem prover. That sounds easy. Joe’s paper showed that this is no easy task at all, and it’s only the beginning.