Research Interests
For a gentle introduction to my research interests, click
here. This will take you on a 10-click
tour that leads back to here.
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.
Some of the questions of interest to me are thus:
- 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.