Skip to main content
PRL Project

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

  • unofficial copies PDF, PS

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

cite link