scientific article; zbMATH DE number 3986665

MaRDI QIDQ3750136zbMATH OpenFDO

Authors Douglas J. Howe

Publication date 1986

zbMATH Keywords

formal reasoningNuprl proof development systemproof constructionreasoning about computationally meaningful mathematics

Mathematics Subject Classification ID

Software, source code, etc. for problems pertaining to number theory (11-04) Software, source code, etc. for problems pertaining to computer science (68-04)

Recommendations

• Implementing constructive real analysis (preliminary report)
• scientific article; zbMATH DE number 4053566
• scientific article; zbMATH DE number 4101139
• Hybrid interactive theorem proving using Nuprl and HOL
• scientific article; zbMATH DE number 4047195

Cited in

(10)

• Type theory and concurrency
• scientific article; zbMATH DE number 1614694 (Why is no real title available?)
• A domain-independent system for modeling number theory using first-order predicate logic
• scientific article; zbMATH DE number 4047195 (Why is no real title available?)
• scientific article; zbMATH DE number 4053566 (Why is no real title available?)
• scientific article; zbMATH DE number 4074542 (Why is no real title available?)
• scientific article; zbMATH DE number 4101139 (Why is no real title available?)
• Exploring abstract algebra in constructive type theory
• Hybrid interactive theorem proving using Nuprl and HOL
• Innovations in computational type theory using Nuprl

Describes a project that uses

Uses Software

• Nuprl

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 Q3750136)