scientific article; zbMATH DE number 1113859

MaRDI QIDQ4375633zbMATH OpenFDO

Authors Douglas J. Howe

Publication date 8 February 1998

zbMATH Keywords

constructive type theoryHOLNuprlsemantics

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 1863394
• Toward sharing libraries of mathematics between theorem provers
• scientific article; zbMATH DE number 4053566
• Hybrid interactive theorem proving using Nuprl and HOL
• Interpreting HOL in the calculus of constructions

Cited in

(10)

• Proof-search in type-theoretic languages: An introduction
• Exercising Nuprl's open-endedness
• Validating Brouwer's continuity principle for numbers using named exceptions
• scientific article; zbMATH DE number 1863394 (Why is no real title available?)
• scientific article; zbMATH DE number 1424013 (Why is no real title available?)
• Hybrid interactive theorem proving using Nuprl and HOL
• An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf
• MBase: Representing knowledge and context for the integration of mathematical software systems
• Importing mathematics from HOL into Nuprl
• Innovations in computational type theory using Nuprl

Describes a project that uses

Uses Software

• Nuprl
• HOL

This page was built for publication:

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