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.
