Importing mathematics from HOL into Nuprl

DOI10.1007/BFB0105410MaRDI QIDQ6567719zbMATH OpenFDO

Authors Douglas J. Howe

Publication date 5 July 2024

Full work available at URL https://doi.org/10.1007/BFB0105410

Mathematics Subject Classification ID

Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Hybrid interactive theorem proving using Nuprl and HOL
• Toward sharing libraries of mathematics between theorem provers
• scientific article; zbMATH DE number 1863394
• scientific article; zbMATH DE number 1113859
• Importing HOL Light into Coq

Cites work

• Edinburgh LCF. A mechanized logic of computation
• Exploring abstract algebra in constructive type theory
• scientific article; zbMATH DE number 3859117 (Why is no real title available?)
• scientific article; zbMATH DE number 512782 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• The \(HOL\) logic extended with quantification over type variables

Cited in

(1)

• Translating HOL-Light proofs to Coq

This page was built for publication: Importing mathematics from HOL into Nuprl

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6567719)