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!
A Theorem Prover for DrScheme
This project involves writing a new theorem prover from scratch. DrScheme is a programming environment for Scheme (and other languages.) It is used in many universities and high schools to teach introductory programming. The philosophy behind this approach is that what students should learn is not a language, but a programming model—and the programming language should support that model and no more. This lets the students learn how to program without getting derailed by advanced features of the target programming language.
One thing DrScheme does not have is a theorem prover. This would be a great enhancement to DrScheme, because it would support reasoning about programs at an early stage. First-year students could write programs in DrScheme, then prove some properties of their programs with a bundled theorem prover. That is what we want to build. Since DrScheme supports several different language levels for pedagogical reasons, the theorem prover will also be developed as a series of different inference engines. This will allow students to understand the reasoning steps taken by the theorem prover. As they gain in logical sophistication, so will the theorem prover, but it must never appear to be simply magical.
A special challenge of this project is that the theorem prover needs to be pedagogically sound. That is, its reasoning should be intelligible to a student. Conversely, things that are obvious to the student should also be obvious to the theorem prover. Both of these are significant challenges, worthy of a Ph.D.
The AKS Algorithm in ACL2
The AKS algorithms is 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.
The goal of this project is to verify that a particular implementation of AKS in Java correctly determines whether a number is prime or composite. This is another collaboration, this time with Mike Gordon, currently at Cambridge. He is best known for his work in Isabelle/HOL, a theorem prover family in the LCF style. He has recently done some work embedding the logic of ACL2 into HOL, in the hope that proofs can be developed based on the extensive work that has already been done in each of these provers. In particular, this project will use existing HOL libraries to establish all the needed facts from number theory, and an existing JVM model in ACL2 to reason about the Java bytecode. Our portion of the work will be mostly on the ACL2 side; one of Gordon's students will take care of the HOL work.
I am especially excited about this project, because it bridges the ACL2 and HOL communities. In my (not so unbiased) opinion, ACL2 and HOL are the premier theorem provers in the world, so an opportunity to work in a project involving both provers is unique.
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.
A Theory of Integration in ACL2
ACL2(r) knows a fair amount of differential calculus, but it knows only one fact from integral calculus: The Fundamental Theorem of Calculus. I am looking for a student who would like to extend ACL2(r)'s knowledge of integral calculus. The goal would be to formalize as much as possible the theory of integration as described in an introductory course on real analysis. A more challenging goal would be to formalize important theorems from vector calculus, e.g., Green's Theorem and Stokes's Theorem. This could easily lead to a Ph.D., though there are also master's-sized pieces that would advance this project significantly.
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 πr2. 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.