Keywords: General Logics, Formal Interoperabilty, Theorem Prover, HOL, Nuprl, Maude, Meta-Tool, HOL-Nuprl Connection, Logic Translator
In this project we investigate the use of general logics introduced by Meseguer 1989 in the context of formal interoperabilty between theorem provers. As a typical and practically relevant example we study the HOL-Nuprl Connection proposed by Doug Howe from a proof-theoretic perspective.
The HOL theorem proving system has a rich library of theories that can save a lot of effort by not having to specify from scratch many commonly encountered theories. Potentially, this is a very useful resource not only for HOL, but for other theorem proving systems based on other logics. Howe defined a map of logics mapping the HOL logic into the logic of Nuprl, and implemented such a mapping to make possible the translation from HOL theories to Nuprl theories. In this way, the practical goal of relating both systems and making the HOL libraries available to Nuprl was achieved. However, the translation itself was carried out by conventional means, and therefore was not in a form suitable for metalogical analysis.
After studying this mapping with the kind help of Doug Howe, Robert Constable and Stuart Allen, we have recently formally specified it in Maude. The result is an executable formal specification of the mapping that translates HOL theories into Nuprl theories. Large HOL libraries have already been translated into Nuprl this way.
In order to verify the correctness of the translation, we have investigated, in parallel with the work summarized above, an abstract version of the mapping in the categorical framework of general logics. In  we have proved a strong correctness result, namely, that the mapping is actually a mapping between the entailment systems of HOL and a classical variant of Nuprl. This result is of a proof-theoretic nature and hence complementary to the semantical argument given by Howe. Beyond its role as a direct justification for the translator, this result suggests an interesting new direction, namely, extending the mapping between entailment systems to a mapping between proof calculi, which would mean in practice that theorems could be translated together with their proofs. Recent progress on the development of such a proof translator on the top of the Nuprl system is reported in the reference  below.