Cardinals in Isabelle/HOL

DOI10.1007/978-3-319-08970-6_8zbMath1416.68152OpenAlexW1821411012MaRDI QIDQ2879247

Andrei Popescu, Jasmin Christian Blanchette, 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

Related Items (10)

Quotients of Bounded Natural Functors ⋮ Unnamed Item ⋮ A Formalized Hierarchy of Probabilistic System Types ⋮ A formalized general theory of syntax with bindings ⋮ Type-theoretic approaches to ordinals ⋮ Unnamed Item ⋮ A formalized general theory of syntax with bindings: extended version ⋮ Unnamed Item ⋮ First steps towards a formalization of forcing ⋮ Generate & Check Method for Verifying Transition Systems in CafeOBJ

Uses Software

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

This page was built for publication: Cardinals in Isabelle/HOL