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

Carsten Schürmann, Mark-Oliver Stehr

Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review

Abstract

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.
Original languageEnglish
Book seriesLecture Notes in Computer Science
Volume4246
ISSN0302-9743
DOIs
Publication statusPublished - 2006

Cite this