Bio. I obtained my PhD from Cornell University in 1988. I was a research associate, and then a faculty member, in the Department of Computer Science at Cornell from 1987 to 1992. From 1992 until 1999, I was a Member of Technical Staff at Bell Labs (part of AT&T, then Lucent) in Murray Hill, New Jersey. I joined the School of Computer Science at Carleton in January 2000. I have served both as Associate Director and Director of the School.
Research Interests. Interactive theorem proving: foundations, design, and implementation of interactive theorem-proving systems; automated reasoning; integrating theorem-provers with other verification tools. Type theory and functional programming languages. Formal methods in software engineering: software verification; verification of "hard" real-time systems.