My research and investigations

Formalize X, Apply Y

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:

  1. 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?
  2. 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.
  3. 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.


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: