Weyl’s Predicative Classical Mathematics as a Logic-Enriched Type Theory

DOI10.1007/978-3-540-74464-1_1MaRDI QIDQ3612432zbMATH OpenOpenAlexFDO

Authors Robin Adams, Zhaohui Luo

Publication date 10 March 2009

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-74464-1_1

zbMATH Keywords

formalisationpredicativismlogic-enriched type theory

Mathematics Subject Classification ID

Foundations of classical theories (including reverse mathematics) (03B30) Mechanization of proofs and logical operations (03B35)

Recommendations

• Weyl's predicative classical mathematics as a logic-enriched type theory
• Classical predicative logic-enriched type theories
• scientific article; zbMATH DE number 49341
• Weyl reexamined: ``Das Kontinuum 100 years later
• The calculus of constructions

Cited in

(6)

• Weyl's predicative classical mathematics as a logic-enriched type theory
• Weyl reexamined: ``Das Kontinuum 100 years later
• Classical predicative logic-enriched type theories
• In the Search of a Naive Type Theory
• A pluralist approach to the formalisation of mathematics
• scientific article; zbMATH DE number 4116496 (Why is no real title available?)

Describes a project that uses

Uses Software

• Plastic
• Twelf

This page was built for publication: Weyl’s Predicative Classical Mathematics as a Logic-Enriched Type Theory

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