We describe a new theorem prover architecture that is intended
to facilitate
mathematical sharing and modularity in formal mathematics and
programming. This system provides
an implementation framework in which multiple logics, including
the Nuprl type theory and the Edinburgh
Logical Framework (LF) can be specified, and even related. The
system provides formal,
object-oriented modules, in which multiple (perhaps mutually inconsistent)
logics can be specified.
Logical correctness is enforced and derived from module dependencies.
Support is provided at a
primitive level for modular proof automation.
The published paper: Postscript, PDF.
A longer version: Postscript, PDF.