Importing mathematics from HOL into Nuprl

Nuprl and HOL are both tactic-based interactive theorem provers for higher-order logic, and both have been used in many substantial applications over the last decade. However, the HOL community has accumulated a much larger collection of formalized mathematics of the kind useful for hardware and software verification. Nuprl’s relative lack impedes its application to verification problems of real practical interest. This paper describes a connection we have implemented between HOL and Nuprl that gives Nuprl effective access to mathematics formalized in HOL. In designing this connection, we had to overcome a number of problems related to differences in the logics, logical infrastructures and stylistic conventions of Nuprl and HOL.