Nuprl-Light: An Implementation Framework for Higher-Order Logics
by Jason Hickey
Proceedings of 14th International Conference on Automated Deduction, W. McCune (ed.), LNAI 1249, pp. 395-399, Springer-Verlag
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.
bibTex ref: Hic97b