Formalising foundations of mathematics
From MaRDI portal
Publication:3094180
DOI10.1017/S0960129511000144zbMath1242.03031OpenAlexW2151140427MaRDI QIDQ3094180
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
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 (13)
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) ⋮ A logical framework perspective on conservativity ⋮ 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
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
This page was built for publication: Formalising foundations of mathematics
