Cardinals in Isabelle/HOL

DOI10.1007/978-3-319-08970-6_8MaRDI QIDQ2879247zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

• Ordinals Cardinals
• Countable Ordinals
• wellorder
• Free Groups
• HOL Light
• HOL
• Isabelle/HOL
• Isabelle

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)