Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.

DOI10.4230/LIPIcs.ITP.2019.9OpenAlexW2978296386MaRDI QIDQ5875415

Cezary Kaliszyk, Karol Pąk, Chad Edward Brown

Publication date: 3 February 2023

Full work available at URL: http://drops.dagstuhl.de/opus/volltexte/2019/11064/pdf/LIPIcs-ITP-2019-9.pdf/

zbMATH Keywords

modelhigher-orderproof foundationTarski Grothendieck

Mathematics Subject Classification ID

Related Items (2)

Isabelle/HOL/GST: a formal proof environment for generalized set theories ⋮ Combining higher-order logic with set theory formalizations

Uses Software

• Isabelle
• Isabelle/HOL
• Mizar
• Isabelle/ZF
• ETPS
• Oz
• Satallax
• Transfer
• Lifting
• kepler98
• Archive Formal Proofs

Cites Work

• Unnamed Item
• Four decades of {\textsc{Mizar}}. Foreword
• Analytic tableaux for higher-order logic with choice
• Brouwer invariance of domain theorem
• Topological manifolds
• 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
• Isabelle import infrastructure for the Mizar Mathematical Library
• An introduction to mathematical logic and type theory: To truth through proof.
• A compendium of continuous lattices in MIZAR
• Semantics of Mizar as an Isabelle object logic
• Classification of alignments between concepts of formal mathematical systems
• Seminar of algebraic geometry du Bois-Marie 1963--1964. Topos theory and étale cohomology of schemes (SGA 4). Vol. 1: Topos theory. Exp. I--IV
• Brouwer Fixed Point Theorem in the General Case
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• How to identify, translate and combine logics?
• Mining the Archive of Formal Proofs
• Sharing HOL4 and HOL Light Proof Knowledge
• Partizan Games in Isabelle/HOLZF
• The Isabelle Framework
• Analytic Tableaux for Simple Type Theory and its First-Order Fragment
• Isabelle Formalization of Set Theoretic Structures and Set Comprehensions
• A FORMAL PROOF OF THE KEPLER CONJECTURE
• Higher-order semantics and extensionality
• Theorem Proving in Higher Order Logics
• General models and extensionality
• A Mechanized Translation from Higher-Order Logic to Set Theory
• Über unerreichbare Kardinalzahlen
• A formulation of the simple theory of types
• Completeness in the theory of types
• General Bindings and Alpha-Equivalence in Nominal Isabelle

This page was built for publication: Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.