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

Carsten Schürmann, Mark-Oliver Stehr

Publikation: Artikel i tidsskrift og konference artikel i tidsskriftTidsskriftartikelForskningpeer review

Abstrakt

Howe’s HOL/Nuprl connection is an interesting example of a translation between two fundamentally different logics, namely a typed higher-order logic and a polymorphic extensional type theory. In earlier work we have established a proof-theoretic correctness result of the translation in a way that complements Howe’s semantics-based justification and furthermore goes beyond the original HOL/Nuprl connection by providing the foundation for a proof translator. Using the Twelf logical 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.
OriginalsprogEngelsk
BogserieLecture Notes in Computer Science
Vol/bind4246
ISSN0302-9743
DOI
StatusUdgivet - 2006

Citationsformater