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

DOI10.1145/1656242.1656246zbMath1351.03002OpenAlexW2093863416WikidataQ130871092 ScholiaQ130871092MaRDI QIDQ2946599

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

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

Related Items (5)

Why Predicative Sets? ⋮ POINCARÉ–WEYL’S PREDICATIVITY: GOING BEYOND ⋮ Classical predicative logic-enriched type theories ⋮ WEYL REEXAMINED: “DAS KONTINUUM” 100 YEARS LATER ⋮ A pluralist approach to the formalisation of mathematics

Uses Software

• Plastic

This page was built for publication: Weyl's predicative classical mathematics as a logic-enriched type theory