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

Skip to Main Content

Apply to the University of Wyoming apply now

Global Resource Navigation

Visit Campus
Download UW Viewbook
Give to UW

Computer Science

College of Engineering and Applied Science

Ruben Gamboa

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
307.766.5190
ruben@uwyo.edu
Ruben Gamboa

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 π 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:

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

Twitter Icon Youtube Icon Instagram Icon Facebook Icon

Accreditation | Emergency Preparedness | Employment at UW | Gainful Employment | Privacy Policy | Accessibility Accessibility information icon