@inproceedings{46478b8cdc5a404aab9098fd9962fecf,
title = "The HOL/NuPRL proof translator a practical approach to formal interoperability",
abstract = "We have developed a proof translator from HOL into a classical extension of NuPRL which is based on two lines of previous work. First, it draws on earlier work by Doug Howe, who developed a translator of theorems from HOL into a classical extension of NuPRL which is justified by a hybrid set-theoretic/computational semantics. Second, we rely on our own previous work, which investigates this mapping from a proof-theoretic viewpoint and gives a constructive meta-logical proof of its soundness. In this paper the logical foundations of the embedding of HOL into this classical extension of NuPRL as well as technical aspects of the proof translator implementation are discussed.",
author = "Pavel Naumov and Stehr, \{Mark Oliver\} and Jos{\'e} Meseguer",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2001.; 14th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2001 ; Conference date: 03-09-2001 Through 06-09-2001",
year = "2001",
doi = "10.1007/3-540-44755-5\_23",
language = "English (US)",
isbn = "354042525X",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "329--345",
editor = "Boulton, \{Richard J.\} and Jackson, \{Paul B.\}",
booktitle = "Theorem Proving in Higher Order Logics - 14th International Conference, TPHOLs 2001, Proceedings",
address = "Germany",
}