Isabelle/HOL/GST: a formal proof environment for generalized set theories

DOI10.1007/978-3-031-16681-5_3arXiv2207.12039OpenAlexW4296050231MaRDI QIDQ6159365

Ciarán Dunne, J. B. Wells

Publication date: 2 June 2023

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2207.12039

zbMATH Keywords

higher-order logicset theoryIsabellesoft types

Mathematics Subject Classification ID

Computer science support for mathematical research and practice (68Vxx)

Cites Work

• Unnamed Item
• The future of logic: foundation-independence
• A consistent foundation for Isabelle/HOL
• Generating custom set theories with non-set structured objects
• Adding an abstraction barrier to ZF set theory
• Semantics of Mizar as an Isabelle object logic
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Mizar’s Soft Type System
• Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.

This page was built for publication: Isabelle/HOL/GST: a formal proof environment for generalized set theories