A Biographical Sketch

An associate professor in the Department of Computer Science of the University of Wyoming, I teach primarily software engineering and software design, but I have also taught algorithms, computer graphics, compilers, networks, enterprise programming, computational number theory, 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 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, and I continue to consult for LIM and develop training materials for Inferdata, Inc. My last full-time job in industry was as the Vice President of Engineering of Loop One, Inc. During the previous 10 years, I worked for LIM as a founder, senior architect, and director. And my start in industry was as a junior researcher in the Deductive Computing Group of MCC.

But there is to more to me than work. I am a skeptic, an erstwhile member of the Committee for the Scientific Investigation of Claims of the Paranormal (CSICOP). However, I choose to believe in extraterrestrials (go ahead, ask me why) and I support SETI and SETI@Home. I am an amateur astronomer who aspires to build his own personal observatory, a science-fiction fan (books, movies, conventions), and a private pilot. I am obsessed with the San Francisco 49ers. I write scientific pieces for the layman and selected diatribes for catharsis. But primarily I am a family man, devoted to my wonderful wife, model daughter, and little boy.