Chief Programmer
Phone: 607-255-8697
Email: eaton@cs.cornell.edu
MS Computer Graphics, Cornell University 1989
I know the code of the entire Nuprl system and have written a large part of it, including the logic engine, structure editor, and formal digital library. I designed and implemented the rule compiler which enables Nuprl to function as a Logical Framework.
I worked on the design of the structure editor with Doug Howe and Stuart Allen and then implemented it and have been improving it from time to time. This included new methods of encoding display specification, a new layout algorithm, many new and improved edit commands, and a new macro facility.
The largest project has been to restructure the system as distributed components. A crucial requirement was to add database ACID properties, including transactions, to the library component. This necessarily required the design and implementation of a communication protocol for the connected components. One innovative feature was the design and implementation of a remote evaluation protocol for ML expressions.
Incrementally I have been adding capabilities to harden theories. This is done mainly by isolating updates to tactic environment and allowing use to be recorded. This allows dependencies to be more transparent. By limiting scope of such updates, greater control over the tactic environment is achieved.
I added a new version of the Auto tactic. One major goal was to improve the ability to control how updates to Auto are used. Additionally, features to support hardening of theories by better isolation of the updates to Auto were included.
I also translated from Coq to Nuprl a formalization of the Resolution algorithm done by Wojciech Moczydlowski.