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 language | English |
---|---|
Book series | Lecture Notes in Computer Science |
Volume | 4246 |
ISSN | 0302-9743 |
DOIs | |
Publication status | Published - 2006 |
Keywords
- Typed higher-order logic
- Polymorphic extensional type theory
- Nuprl connection
- Howe's HOL
- Proof translator
- Twelf logical framework