Ruben Gamboa

Professor and Head of Computer Scienceruben-scope

Room 4085, 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

 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

  • Head of Computer Science, University of Wyoming, 2019-present.
  • 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

  • Proving Lindemann’s theorem and the transcendence of \(e\) and \(\pi\) in ACL2(r).
  • A formal proof in ACL2(r) of the three classical impossible constructions of geometry.
  • A formalization of the Banach-Tarski Paradox in ACL2(r).
  • A formalization of the Prime Number Theorem in ACL2(r).

Selected Publications

  • Page, R. and R. Gamboa. Essential Logic for Computer Science. MIT Press. 2019.
  • 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. “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.
  • 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.