Importing mathematics from HOL into Nuprl

DOI10.1007/BFB0105410zbMATH Open1543.68419MaRDI QIDQ6567719FDOQ6567719

Authors: Douglas J. Howe 

Publication date: 5 July 2024

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

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Edinburgh LCF. A mechanized logic of computation
• Title not available (Why is that?)
• Exploring abstract algebra in constructive type theory
• Title not available (Why is that?)
• The \(HOL\) logic extended with quantification over type variables

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)