Combining higher-order logic with set theory formalizations
From MaRDI portal
Publication:6161232
DOI10.1007/s10817-023-09663-5OpenAlexW4377965362MaRDI QIDQ6161232
Publication date: 27 June 2023
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-023-09663-5
Cites Work
- Unnamed Item
- Unnamed Item
- Four decades of {\textsc{Mizar}}. Foreword
- Brouwer invariance of domain theorem
- Topological manifolds
- A revision of the proof of the Kepler conjecture
- Set theory for verification. I: From foundations to functions
- Isabelle/HOL. A proof assistant for higher-order logic
- Aligning concepts across proof assistant libraries
- The role of the Mizar mathematical library for interactive proof development in Mizar
- From types to sets by local type definition in higher-order logic
- Refinement to imperative HOL
- A compendium of continuous lattices in MIZAR
- Grothendieck universes
- A tale of two set theories
- The univalence axiom in cubical sets
- Semantics of Mizar as an Isabelle object logic
- Classification of alignments between concepts of formal mathematical systems
- Brouwer Fixed Point Theorem in the General Case
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Univalent Semantics of Constructive Type Theories
- How to identify, translate and combine logics?
- HOL Light: An Overview
- Mining the Archive of Formal Proofs
- Sharing HOL4 and HOL Light Proof Knowledge
- Partizan Games in Isabelle/HOLZF
- The Isabelle Framework
- Code Generation via Higher-Order Rewrite Systems
- Constructive Type Classes in Isabelle
- Isabelle Formalization of Set Theoretic Structures and Set Comprehensions
- Cubical methods in homotopy type theory and univalent foundations
- Type Theory and Homotopy
- Mathematical Knowledge Management
- Theorem Proving in Higher Order Logics
- A Mechanized Translation from Higher-Order Logic to Set Theory
- Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
- Declarative Proof Translation (Short Paper)
- Verified analysis of random binary tree structures
