Some of the content on this website requires JavaScript to be enabled in your web browser to function as intended. While the website is still usable without JavaScript, it should be enabled to enjoy the full interactive experience.

Skip to Main Navigation. Each navigation link will open a list of sub navigation links.

Skip to Main Content

Computer Science|College of Engineering and Applied Science

Ruben Gamboa

Associate 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

For more information visit Dr. Gamboa's homepage.

Ruben Gamboa


  • 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

  • Associate Professor, University of Wyoming, 2007-present
  • 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 π 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.

Share This Page:

Footer Navigation

University of Wyoming Medallion
1000 E. University Ave. Laramie, WY 82071 // UW Operators (307) 766-1121 // Contact Us // Download Adobe Reader