Ruben Gamboa

Professor of Computer Scienceruben-scope

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


  • 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

Conference Organization and Editorial Work

  • 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

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