Research with ACL2

ACL2 LogoACL2 is a theorem prover over a first-order logic based on the programming language Common Lisp. To prove theorems with ACL2, a user must first define Common Lisp functions that describe the relevant theory, e.g., functions for manipulating elements of a field. The user can also submit theorems and lemmas that ACL2 attempts to prove. Compared to other theorem provers, ACL2 is a remarkably independent theorem prover. Nevertheless, the user will almost certainly have to guide ACL2 either implicitly, by adding useful lemmas to ACL2’s database, or explicitly, by giving ACL2 direct hints to help it find the proof the user has in mind.

My research interests in ACL2 include providing support for real analysis with ACL2(r), a variant of ACL2 that I developed as part of my dissertation work, and formalizations of interesting (to me) theorems in mathematics and computer science. Since joining the University of Wyoming, I have had the chance to collaborate with John Cowles on several formalizations in ACL2 and ACL2(r).

I am an active member of the ACL2 community. I have published research papers in nearly all ACL2 Workshops, and I have served in the program committee or some other capacity in many of them, as well. In 2006, I was the publications chair for the ACL2 Workshop, and in 2007 and 2013 I served as workshop co-chair. In 2014, I was co-chair of the conference on Interactive Theorem Proving (ITP), which has a longstanding relationship with the ACL2 community. I have also served two terms on the ACL2 Steering Committee.

If you are a graduate student looking for an interesting project for either a Master’s or Ph.D., you may want to consider doing some ACL2-related work with me. Check out my Help Wanted! page for some suggestions.

Leave a Reply