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

    Keywords

    • Typed higher-order logic
    • Polymorphic extensional type theory
    • Nuprl connection
    • Howe's HOL
    • Proof translator
    • Twelf logical framework

    Fingerprint

    Dive into the research topics of 'An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework'. Together they form a unique fingerprint.

    Cite this