A Biographical Sketch

I am an assistant professor in the Department of Computer Science of the University of Wyoming. Primarily I teach software engineering and software design, but I have also taught computer graphics, networks, enterprise programming, and even a course on my primary research area, automated reasoning.

My most prolific research area involves theorem proving, in particular with 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.

I am currently seeking students at all levels who can help me with one of several research projects. Take a look at my Help Wanted! page for information on these projects.

I am in academia because I am passionate about K-16 education, firmly believing that education is the way to a better future for the individuals who are educated and for the community as a whole. I take my duties as a college educator seriously, and I volunteer some of my time to teach elementary school students about computers and astronomy, which I consider to be a "gateway drug to science," in Pamela Gay's immortal phrase. I have recently been appointed to the adjunct faculty of the Science and Mathematics Teaching Center (SMTC) at UW. As a member of the SMTC, I am planning a project that will use distance learning technology to promote astronomy and computer knowledge to Wyoming students. Come and talk to me about it if you are interested.

I spent 15 years in industry before joining academia, and I continue to consult for LIM and run occasional training seminars for Inferdata, Inc. My last full-time job in industry was as the Vice President of Engineering of Loop One, Inc. 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 work and academics are not all there is to me. 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—come to Denvention 3, the World Science Fiction Convention in Denver in 2008), 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.