Formalising foundations of mathematics

DOI10.1017/S0960129511000144zbMath1242.03031OpenAlexW2151140427MaRDI QIDQ3094180

Mihnea Iancu, Florian Rabe

Publication date: 21 October 2011

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129511000144

zbMATH Keywords

foundations of mathematicsformalisation of mathematicslogical frameworks

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Foundations of classical theories (including reverse mathematics) (03B30) Axiomatics of classical set theory and its fragments (03E30)

Related Items

A Proof Theoretic Interpretation of Model Theoretic Hiding ⋮ Towards Logical Frameworks in the Heterogeneous Tool Set Hets ⋮ A scalable module system ⋮ The Mizar Mathematical Library in OMDoc: translation and applications ⋮ An Axiomatic Value Model for Isabelle/UTP ⋮ A logical framework combining model and proof theory ⋮ A Foundational View on Integration Problems ⋮ Project Abstract: Logic Atlas and Integrator (LATIN) ⋮ Isabelle/UTP: A Mechanised Theory Engineering Framework ⋮ A pluralist approach to the formalisation of mathematics ⋮ On the fine-structure of regular algebra ⋮ The future of logic: foundation-independence

Uses Software

• Isabelle/HOL
• Mizar

Cites Work

• Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics
• The calculus of constructions
• IMPS: An interactive mathematical proof system
• Structured theory presentations and logic representations
• Mizar’s Soft Type System
• An Interpretation of Isabelle/HOL in HOL Light
• Combining Type Theory and Untyped Set Theory
• Refinement Types as Proof Irrelevance
• A framework for defining logics
• On the Structure of Mizar Types
• Importing HOL Light into Coq
• A Mechanized Translation from Higher-Order Logic to Set Theory
• Classical Logic with Partial Functions
• A formulation of the simple theory of types