Formalizations with ACL2 and ACL2(r)
One of my research goals is the formalization of interesting (to me) theorems from mathematics and computer science. Currently, I am working on a formalization of approximation algorithms to the Set Cover problem. The following table lists some of the formalizations that I, or one of my collaborators, have done in the past.
| Project | Author(s) | Availability |
|---|---|---|
| Irrationality of Square Root | Ruben Gamboa | ACL2 Distribution |
| Exponential Function | Ruben Gamboa | ACL2 Distribution |
| Trigonometric Functions | Ruben Gamboa | ACL2 Distribution |
| Fast Fourier Transform | Ruben Gamboa | ACL2 Distribution |
| Mean Value Theorem | Ruben Gamboa | ACL2 Distribution |
| Taylor's Theorem | Ruben Gamboa Brittany Middleton |
|
| Correctness of Hardware Implementation of SQRT | Jun Sawada Ruben Gamboa |
|
| Correctness of a Kalman Filter Implementation | Ruben Gamboa John Cowles Jeff Van Baalen |
|
| Cook-Levin Theorem | Ruben Gamboa John Cowles |
|
| Powerlist Data Structure | Ruben Gamboa | ACL2 Distribution |
| Red-Black Trees | Ruben Gamboa | DrACuLa Distribution |