Weyl's predicative classical mathematics as a logic-enriched type theory

DOI10.1145/1656242.1656246MaRDI QIDQ2946599zbMATH OpenOpenAlexWikidataFDO

Authors Robin Adams, Zhaohui Luo

Publication date 17 September 2015

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1656242.1656246

zbMATH Keywords

formalization of mathematicspredicativismlogic-enriched type theories

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 1342281
• scientific article; zbMATH DE number 3521950
• Publication:4731167
• Mathematical logic: proof theory, type theory and constructive mathematics
• Predicate logics of constructive mathematical theories
• scientific article; zbMATH DE number 1984270
• Type logics and pregroups
• Higher-Order Logic and Type Theory

Cited in

(7)

• A pluralist approach to the formalisation of mathematics
• POINCARÉ–WEYL’S PREDICATIVITY: GOING BEYOND
• Why Predicative Sets?
• Weyl’s Predicative Classical Mathematics as a Logic-Enriched Type Theory
• A refinement of de Bruijn's formal language of mathematics
• Weyl reexamined: ``Das Kontinuum 100 years later
• Classical predicative logic-enriched type theories

Describes a project that uses

Uses Software

• Plastic

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