Research Interests

Last updated: 4/9/01

Machine-assisted mathematical proofs, specifically with HOL:

I am currently engaged, and look to continue to be so for some time, in a project to turn the early sections of Saunders Mac Lane's Categories for the Working Mathematician into HOL. The only product of this work ready for release as of Spring 2001 is a collection of general-purpose (not category-related) HOL tactics, of which documentation and ML source with signature are available. For other local HOL-related material, see the CASE Center Formal Methods Group page.


Other Research Interests:

Functional programming

Types and polymorphism

Applications of category theory to data structures

Combinatorial games

Computational geometry and solid modelling