Cardinals in Isabelle/HOL
From MaRDI portal
Publication:2879247
DOI10.1007/978-3-319-08970-6_8zbMATH Open1416.68152OpenAlexW1821411012MaRDI QIDQ2879247FDOQ2879247
Authors: Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel 
Publication date: 8 September 2014
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://eprints.mdx.ac.uk/15164/2/card.pdf
Recommendations
- Ordinals in HOL: transfinite arithmetic up to (and beyond) \(\omega _{1}\)
- Formalizing ordinal partition relations using Isabelle/HOL
- Mechanizing set theory. Cardinal arithmetic and the axiom of choice
- scientific article; zbMATH DE number 7204430
- Irrationality and transcendence criteria for infinite series in Isabelle/HOL
Cited In (13)
- Type-theoretic approaches to ordinals
- Formalizing ordinal partition relations using Isabelle/HOL
- First steps towards a formalization of forcing
- Generate \& check method for verifying transition systems in CafeOBJ
- A formalized general theory of syntax with bindings
- Title not available (Why is that?)
- A formalized general theory of syntax with bindings: extended version
- Places, lists, aggregates
- Modal logics for nominal transition systems
- Quotients of Bounded Natural Functors
- Title not available (Why is that?)
- A formalized hierarchy of probabilistic system types. Proof pearl
- Ordinals in HOL: transfinite arithmetic up to (and beyond) \(\omega _{1}\)
Uses Software
This page was built for publication: Cardinals in Isabelle/HOL
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2879247)
