Cardinals in Isabelle/HOL
From MaRDI portal
Publication:2879247
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
- A formalized general theory of syntax with bindings: extended version
- scientific article; zbMATH DE number 7204430 (Why is no real title available?)
- Places, lists, aggregates
- Modal logics for nominal transition systems
- Quotients of Bounded Natural Functors
- scientific article; zbMATH DE number 7471712 (Why is no real title available?)
- A formalized hierarchy of probabilistic system types. Proof pearl
- Ordinals in HOL: transfinite arithmetic up to (and beyond) \(\omega _{1}\)
Describes a project that uses
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)