Help Wanted!


Overview of the Projects

  • Are you a graduate student looking for a Master’s project or Ph.D. thesis, or an undergraduate student looking for a capstone project for COSC4950 & 4955?
  • Do you think math is fun?
  • Do you like to write complicated programs?
  • Do you believe that functional programming was invented by God, and all other paradigms are the work of man?
  • Do you like working long hours on hard problems?

If you answer “yes!” to these questions, I may have a project for you. I am working on a few different projects, and I can use some help in all of them. Each project has different tasks of different sizes, so it doesn’t matter whether you are looking for a Ph.D. or an undergraduate capstone project. If you’re interested, and if you have a solid background in math and functional programming, you can help.

Keep in mind, however, that these projects are not currently supported by outside funds, so I cannot offer you an RA position to work on them right now. If you’re a Ph.D. student looking for funding, I recommend that you consider a TA position instead of an RA. Then if you’re interested in working on one of these projects for your dissertation, we can work on securing funding together.

How to Join

If you’re interested in any of these projects, or in other verification projects with ACL2 or ACL2(r), send me some e-mail or drop by my office. Let’s talk!

Transcendental Functions

Transcendental Functions in ACL2

This project involves the verification of mathematical algorithms in ACL2(r). Specifically, this involves verifying that several infinite sums converge to specified values. This also involves reasoning about some transcendental functions, like logs, roots, and trigonometric functions. And there’s lots of work formalizing various bits of mathematics, like the mean value theorem or some convergence results. This project is part of a collaboration with David Russinoff of AMD, and it has great practical value. The larger goal is to verify the algorithms implemented in AMD’s chips that approximate the transcendental functions.

Fourier Series

Fourier Series in ACL2

I have previously formalized that the Fast Fourier Transform correctly computes the Fourier Transform of a vector. It would be very interesting to prove that the Fourier Transform of a periodic function converges to it.  Moreover, it would be very nice to tie in my previous FFT result by formalizing the Discrete Fourier Transform and showing that it satisfies the definition of the Fourier Transform in that theorem. For a Ph.D., these results can be extended to include error analysis when floating-point numbers are used to compute the FFT.


Formalizing Mathematics in ACL2

There are numerous projects that fall into this category, and many of these require only a limited amount of mathematical knowledge. Here’s one I’d like to work on: show that the area of a circle with radius \(r\) is \(\pi r^2\). This one is actually challenging, and it draws on some interesting results from analysis. There really are a number of mathematical facts that are accessible and that you can formalize for a capstone or master’s thesis.

Another interesting formalization is the AKS algorithm, the famous polynomial-time algorithm for deciding if a number is prime or composite. For a long time, it was conjectured that no such algorithm existed. Surprisingly, AKS uses only a small amount of number theory to solve the problem in polynomial time. This would be a fantastic algorithm to verify in ACL2.

Leave a Reply