Ruben Gamboa

Educational Background

Dr. Gamboa received his Ph.D. from the University of Texas at Austin uinder the supervision of Dr. Robert S. Boyer. He is the author and maintainer of the ACL2(r) variant of the theorem prover ACL2, and he is recognized as an expert in the formalization of mathematics with ACL2. His interests are very broad, encompassing almost all aspects of computer science. Beyond that, he has a lifelong love of mathematics, physics, and astronomy. In fact, he is an amateur astronomer who dabbles in astrophotography. He is also a passionate educator and a strong believer in the power of education to change people’s lives for the better. As part of his educational mission, he serves as the ABET coordinator for the Computer Science program at UW, and he is a member of ABET's Computing Accreditation Commision. 

 

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.