Formalising foundations of mathematics

DOI10.1017/S0960129511000144MaRDI QIDQ3094180zbMATH OpenOpenAlexFDO

Authors 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

formalisation of mathematicsfoundations of mathematicslogical frameworks

Mathematics Subject Classification ID

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

Recommendations

• A pluralist approach to the formalisation of mathematics
• A mechanized translation from higher-order logic to set theory
• Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics
• Preface to the special issue: Interactive theorem proving and the formalization of mathematics
• A logical framework for developing and mechanizing set theories

Cites work

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

Cited in

(24)

• Making PVS accessible to generic services by interpretation in a universal format
• The Mizar Mathematical Library in OMDoc: translation and applications
• On the fine-structure of regular algebra
• Mathematical forms and forms of mathematics: leaving the shores of extensional mathematics
• The future of logic: foundation-independence
• Isabelle/UTP: a mechanised theory engineering framework
• A proof theoretic interpretation of model theoretic hiding
• Towards logical frameworks in the heterogeneous tool set Hets
• An Axiomatic Value Model for Isabelle/UTP
• A pluralist approach to the formalisation of mathematics
• Formal systems of constructive mathematics
• Formal logic definitions for interchange languages
• A scalable module system
• scientific article; zbMATH DE number 1951637 (Why is no real title available?)
• scientific article; zbMATH DE number 1418078 (Why is no real title available?)
• Formalizing Scientifically Applicable Mathematics in a Definitional Framework
• A foundational view on integration problems
• Project abstract: logic atlas and integrator (LATIN)
• scientific article; zbMATH DE number 4197450 (Why is no real title available?)
• A logical framework combining model and proof theory
• A mechanized translation from higher-order logic to set theory
• A logical framework perspective on conservativity
• N. G. de Bruijn's contribution to the formalization of mathematics
• Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics

Describes a project that uses

Uses Software

• Isabelle/HOL
• Mizar

This page was built for publication: Formalising foundations of mathematics

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