Ruben Gamboa
Ruben Gamboa
Professor
Computer Science
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
Research Interests
- ACL2, formalization of mathematics, automated theorem proving, applications of cloud
computing and NoSQL databases
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
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.
