Education #

• Ph.D. Computer Science, University of Texas at Austin, 1999.
• M.S. Astronomy, Swinburne Technical University (Online), 2013.
• M.C.S. Computer Science, Texas A&M University, 1986.
• B.S. Computer Science, Angelo State University, 1984.

Professional Experience #

• Head of Computer Science, University of Wyoming, 2019-2022.
• Professor, University of Wyoming, 2015-present.
• Associate Professor, University of Wyoming, 2007-2015.
• Assistant Professor, University of Wyoming, 2002-2007.
• Consultant, Kestrel Institute, 2021-present.
• Member, Technical Advisory Group, Morningstar, 2010-2011.
• Member, Technical Advisory Board, Logical Information Machines (LIM), 2000-2010.
• V.P. of Engineering, Loop One, 2000-2001.
• Founder and Member of Board of Directors, Logical Information Machines (LIM), 1990-2000.
• Junior Member, Technical Staff, Microelectronics and Computer Technology Corporation (MCC), 1988-1989.

Research Interests #

ACL2, formalization of mathematics, automated theorem proving, applications of cloud computing and NoSQL databases.

Current Research Projects #

• Using machine learning to guide ACL2 proof attempts (with Kestrel).
• Proving Lindemann’s theorem and the transcendence of 𝑒 and 𝜋 in ACL2(r).
• A formal proof in ACL2(r) of the three classical impossible constructions of geometry.
• A formalization of Bertrand's Postulate in ACL2(r).
• A formalization of the Prime Number Theorem in ACL2(r).

Selected Publications #

• Bapanapally, J. and R. Gamboa. “A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(r)”. In Proceedings of the 13th Interactive Theorem Proving - Thirteenth International Conference, ITP 2022, Haifa, Israel, July 31–Aug 12, 2022.
• Gamboa, R. and W. Gamboa. “All Prime Numbers Have Primitive Roots”. In: Proceedings of the Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, May 26–27, 2022. Ed. by R. Sumners and C. Chau. Electronic Proceedings in Theoretical Computer Science.
• Gamboa, R. and A. Thoney. “Using ACL2 To Teach Students About Software Testing”. In: Proceedings of the Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, May 26–27, 2022. Ed. by R. Sumners and C. Chau. Electronic Proceedings in Theoretical Computer Science.
• Gamboa, R., J. Cowles, and W. Gamboa. “Quadratic Extensions in ACL2”. In: Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications, Worldwide, Planet Earth, May 28–29, 2020. Ed. by G. Passmore and R. Gamboa. Electronic Proceedings in Theoretical Computer Science.
• Page, R. and R. Gamboa. Essential Logic for Computer Science. MIT Press. 2019.
• Gamboa, R. and J. Cowles. “The Fundamental Theorem of Algebra in ACL2.” In Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, TX, 2018.
• Buss, A. and R. Gamboa. Teacher Transformations in Developing Computational Thinking: Gaming and Robotics Use in After-School Settings.” In Emerging Research, Practice, and Policy on Computational Thinking. Ed. by P. Rich and C. Hodges. Springer. 2017.
• Gamboa, R. and J. Cowles. “Formal Verification of Medina’s Sequence of Polynomials for Approximating Arctangent.” In Proceedings of the 12th International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 2014.
• Cowles, J. and R. Gamboa. “Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis.” In Proceedings of the 12th International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, Austria, 2014.
• Gamboa, R. and J. Cowles. “A Cantor Trio: Denumerability, the Reals, and the Real Algebraic Numbers.” In Proceedings of the 3rd International Conference on Interactive Theorem Proving (ITP), Princeton, NJ, 2012.
• Reid, P. and R. Gamboa. “Automatic Differentiation in ACL2.” In Proceedings of the 2nd International Conference on Interactive Theorem Proving (ITP), Nijmegen, The Netherlands, 2011.
• Gamboa, R. and J. Cowles. “Inverse Functions in ACL2(r).” In 8th International Workshop on the ACL2 Theorem Prover and its Applications, Boston, MA, 2009.
• Gamboa, R. and J. Cowles. “The Chain Rule and Friends in ACL2(r).” Presented at the 8th International Workshop on the ACL2 Theorem Prover and its Applications, Boston, MA, 2009.
• Gamboa, R. and J. Cowles. “Theory Extension in ACL2(r).” In Journal of Automated Reasoning, May, 2007.
• Gamboa, R. “ACL2.” In The Seventeen Provers of the World, by F. Wiedijk. Springer, Lecture Notes in Artificial Intelligence, 2006.
• Gamboa, R. and J. Cowles. “A Mechanical Proof of the Cook-Levin Theorem.” In Proceedings of the 17th International Conference on Theorem Proving and Higher Order Logics (TPHOLs), Park City, UT, 2004.
• Sawada, J. and R. Gamboa. “Mechanical Verification of a Square Root Algorithm using Taylor’s Theorem.” In Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design (FMCAD), Portland, OR, 2002.
• Gamboa, R. and B. Middleton. “Taylor’s Formula with Remainder.” In 3rd International Workshop on the ACL2 Theorem Prover and its Applications, Grenoble, France, 2002.
• Gamboa, R. and M. Kaufmann. “Non-Standard Analysis in ACL2.” In Journal of Automated Reasoning, November, 2001.
• Gamboa, R. “Mechanically Verifying the Correctness of the Fast Fourier Transform in ACL2.” In the Workshop on Parallel Programming, part of the 1st Merged Symposium of the International Parallel Processing Symposium and the Symposium on Parallel and Distributed Processing (IPPS/SPDP), Orlando, FL, 1998.
• Chimenti, D., R. Gamboa et al. “The LDL System Prototype.” In IEEE Transactions on Data and Knowledge Engineering, March, 1990.

Conference Organization and Editorial Work #

• Co-chair of the 16th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, 2020.
• Co-editor of a special issue on Interactive Theorem Proving of the Journal of Automated Reasoning.
• Co-chair of the 5th Conference on Interactive Theorem Proving and Related Issues (ITP), Vienna, Austria, 2014.
• Co-chair of the 11th International Workshop on the ACL2 Theorem Prover and its Applications, Laramie, Wyoming, 2013.
• Co-chair of the 7th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, 2007.

Grants Awarded #

• Leonard, J., R. Gamboa, G. Verma, R. Ellington, B. Gellis. “The Bessie Coleman Project–Using Computer Modeling and Flight Simulation to Create STEM Pathways,” NSF DRL-1757976, $1,199,884.
• Ipina, L., R. Gamboa, and D. Stanescu. “CS 10K: Beauty and Joy, Adapted and Adopted: Building a Computational Teaching Cadre from within Wyoming Schools,” NSF CNS-1441069, 1/1/15-12/31/17, $587,947.
• Leonard, J., S. Aryana, M. Chamberlin, S. Chamberlin, M. Clementz, and K. Wells. “Collaborative Research: Wyoming Interns to Teacher Scholars (WITS) Program,” NSF DUE-1439546, 10/1/14-9/30/19, $1,449,116. R. Gamboa listed under “Key Personnel.”
• Leonard, J., A. Buss, R. Gamboa, J. Hamaan, and F. Jafari. “Visualization Basics: Using Gaming to Improve Computational Thinking,” NSF DRL-1311810, 10/01/13-9/20/16. $1,1999,963.
• Mueller, S. and R. Gamboa. “CSUMS: A Pilot Program to Train Cryptography Students in Computation,” NSF DMS-0639325, 9/13/06-8/31/08, $196,000.
• Gamboa, R. and J. Caldwell. “SoD-HCER: Comprehensibility as a Design Criterion,” NSF CNS-0613919, 9/1/06-8/31/08 (extended to 8/31/09), $157,428.
• Van Baalen, J. and R. Gamboa. “Video Analysis and Content Exploitation (VACE),” Disruptive Technology Office (DTO), 1/15/07-8/31/10, $576,000. Terminated 9/1/07 when the DTO decided to make all VACE-related work classified.
• Gamboa, R. “Logical Information Machines Next-Generation Time Series.” LIM8277, 9/1/03-5/31/06, $102,957.
• Cowles, J., R. Gamboa, and J. Van Baalen. “Mechanical Verification of Synthesized Code.” NASA NAG 2-1570, 7/15/02-10/14/03, $26,387.
• Caldwell, J., R. Gamboa, and J. Van Baalen. “MRI: Acquisition of a Network of Workstations Serving as a Platform for Distributed Automated Reasoning.” NSF EIA-0216592, 7/1/02-6/30/05, $82,530.