Another way to get a quick glimpse of my research interests is to see ``My'' Best Ideas.

I am interested in

- mechanical theorem proving, and
- its use to verify computing systems.

- Can an axiomatically defined applicative programming language serve effectively as a specification/modeling language?
- Can we build a mechanical theorem prover that is
- sound,
- powerful,
- extensible,
- easy for the novice to learn, and
- incredibly fun to use?

- Can we formalize enough of mathematics and computer science so that proofs of interesting systems can be routinely checked?
- How can our technology be used to verify our theorem prover and its implementation?

Return to home page.