An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework

Howe's HOL/Nuprl connection is an interesting example of a translation between two fundamentally dierent logics, namely a typed higher-order logic and a polymorphic extensional type theory. In ear- lier work we have established a proof-theoretic correctness result of the translation in a way that complements Howe's semantics-based justifica- tion and furthermore goes beyond the original HOL/Nuprl connection by providing the foundation for a proof translator. Using the Twelf log- ical framework, the present paper goes one step further. It presents the first rigorous formalization of this treatment in a logical framework, and hence provides a safe alternative to the translation of proofs.