NuPRL-Light: An implementation framework for higher-order logics.
In William McCune, editor, Proceedings of the 14th International Conference on Automated Deduction, volume 1249 of Lecture Notes in Artificial Intelligence, pages 395–399. Springer, July 13–17 1997.
PDF (181 KB), PostScript (229 KB).
An extended version of the paper can be found at http://www.cs.caltech.edu/~jyh/papers/cade14_nl/default.html}.
Note: "NuPRL-Light" is the former name of the MetaPRL Theorem Prover.
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.