The HOL/NuPRL proof translator a practical approach to formal interoperability

Pavel Naumov, Mark Oliver Stehr, José Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationTheorem Proving in Higher Order Logics - 14th International Conference, TPHOLs 2001, Proceedings
EditorsRichard J. Boulton, Paul B. Jackson
PublisherSpringer-Verlag
Pages329-345
Number of pages17
ISBN (Print)354042525X, 9783540425250
StatePublished - Jan 1 2001
Externally publishedYes
Event14th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2001 - Edinburgh, United Kingdom
Duration: Sep 3 2001Sep 6 2001

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2152
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other14th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2001
CountryUnited Kingdom
CityEdinburgh
Period9/3/019/6/01

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'The HOL/NuPRL proof translator a practical approach to formal interoperability'. Together they form a unique fingerprint.

  • Cite this

    Naumov, P., Stehr, M. O., & Meseguer, J. (2001). The HOL/NuPRL proof translator a practical approach to formal interoperability. In R. J. Boulton, & P. B. Jackson (Eds.), Theorem Proving in Higher Order Logics - 14th International Conference, TPHOLs 2001, Proceedings (pp. 329-345). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2152). Springer-Verlag.