Short Bio

rubenAs department head of the Department of Computer Science of the University of Wyoming, most of my time is spent making sure our department is running smoothly and that its activities are aligned with the needs of our many constituents. I’m especially interested in finding ways to make computer science more central to the university. But I still consider teaching to be my top priority, even though these days I only get to teach the discrete math course and a high school course on AP Computer Science Principles. In the past, I taught databases, software engineering, software design, algorithms, computer graphics, compilers, networks, enterprise programming, computational number theory, the senior capstone course, and even a course on my research area—automated reasoning. Through UW’s honors program, I have also taught courses exploring the emergence of a digital society and the possibility of automated artists.

My primary research area involves theorem proving, modifying and using the theorem prover ACL2. For my dissertation, under the supervision of Bob Boyer, I created ACL2(r), a variant of ACL2 that uses non-standard analysis to formalize the irrational numbers. I have since used ACL2 and ACL2(r) to prove several different theorems, such as the impossibility of certain classical geometric constructions (like trisecting an angle), the Fundamental Theorem of Algebra, Taylor’s Theorem, and the Cook-Levin Theorem. I am also interested in other applications of theorem proving. See my research overview for details.

Students: If you are looking for a topic for a graduate thesis or an undergraduate project, take at look at my Help Wanted! page. I have several ideas looking for good students!

I spent 15 years in industry before joining academia. My last full-time job in industry was as the Vice President of Engineering of Loop One, Inc, which was then acquired by Neopost. During the previous 10 years, I worked for LIM as a founder, senior architect, and director. After Morningstar acquired LIM, I served a term on Morningstar’s  Technical Advisory Board. My start in industry was as a junior researcher in the Deductive Computing Group of MCC.

But I am not all about work. I am a skeptic, an erstwhile member of the Committee for the Scientific Investigation of Claims of the Paranormal (CSICOP). Yet I choose to believe in extraterrestrials (go ahead, ask me why) and I support SETI and SETI@Home. I am an amateur astronomer who wishes he had more time to enjoy his personal observatory, a science-fiction fan (books, movies, conventions), and a private pilot—though Wyoming’s winds keep me grounded. I love the Denver Broncos. I write scientific pieces for the layman and selected diatribes for catharsis. And above all, I’m devoted to my wife and two kids, whom I miss dearly, now that they are both away to college. #emptynest