scientific article; zbMATH DE number 4053566

MaRDI QIDQ3789525zbMATH OpenFDO

Authors Douglas J. Howe

Publication date 1988

zbMATH Keywords

constructive mathematicsformal metamathematicsNuprltheorem provingtype theory

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Second- and higher-order arithmetic and fragments (03F35)

Recommendations

• scientific article; zbMATH DE number 3986665
• Innovations in computational type theory using Nuprl
• Towards a formally verified proof assistant
• scientific article; zbMATH DE number 4155932
• scientific article; zbMATH DE number 4101139

Cited in

(16)

• Metacircularity in the polymorphic \(\lambda\)-calculus
• Program tactics and logic tactics
• Nuprl
• A metatheory of a mechanized object theory
• Metainferential reasoning on strong Kleene models
• Towards a formally verified proof assistant
• scientific article; zbMATH DE number 3986665 (Why is no real title available?)
• scientific article; zbMATH DE number 4101139 (Why is no real title available?)
• scientific article; zbMATH DE number 50754 (Why is no real title available?)
• scientific article; zbMATH DE number 1301854 (Why is no real title available?)
• scientific article; zbMATH DE number 1113859 (Why is no real title available?)
• Some normalization properties of Martin-Löf's type theory, and applications
• A verified theorem prover backend supported by a monotonic library
• Formal program optimization in Nuprl using computational equivalence and partial types
• Proof by computation in the Coq system
• Innovations in computational type theory using 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 Q3789525)