**Professor of Computer Science**

Room 4084B, Engineering Building

University of Wyoming

College of Engineering and Applied Science

Department of Computer Science

Dept. 3315

1000 E. University Avenue

Laramie, WY 82071

ruben@uwyo.edu

University of Wyoming

College of Engineering and Applied Science

Department of Computer Science

Dept. 3315

1000 E. University Avenue

Laramie, WY 82071

ruben@uwyo.edu

** Education**

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

**Professional Experience**

- Professor, University of Wyoming, 2015-present.
- Associate Professor, University of Wyoming, 2007-2015.
- Assistant Professor, University of Wyoming, 2002-2007.
- 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**

- Continuing the ACL2(r) formalization of the transcendental functions in the x86 instruction set. This project is motivated by work of David Russinoff originally at AMD and now at Intel.
- Continuing the formalization of various sequences and series in ACL2(r). Of particular interest are the convergence and divergence of summations of reciprocals of various sets of numbers, e.g., primes.
- Proving Lindemann’s theorem and the transcendence of \(e\) and \(\pi\) in ACL2(r). This project is in support of a practical verification effort at Intel.
- Exploring the formalization of analog circuits in ACL2(r). This project is of interest to engineers at Centaur Technology, who use formal methods to reason about digital designs and would like a similar support for analog design.

**Selected Publications**

- 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-editor of a forthcoming Festschrift in honor of Robert Boyer and J Moore.
- Co-editor of a forthcoming 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**

- 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.