Cardinals in Isabelle/HOL

Conference paper

Blanchette, J., Popescu, A. and Taytel, D. 2014. Cardinals in Isabelle/HOL. 5th International Conference on Interactive Theorem Proving. Vienna, Austria 14 - 17 Jul 2014 Springer. pp. 111-127
TypeConference paper
TitleCardinals in Isabelle/HOL
AuthorsBlanchette, J., Popescu, A. and Taytel, D.
Abstract

We report on a formalization of ordinals and cardinals in Isabelle/HOL. A main challenge we faced was the inability of higher-order logic to represent ordinals canonically, as transitive sets (as done in set theory). We resolved this into a “decentralized” representation identifying ordinals with well-orders, with all concepts and results proved to be invariant under order isomorphism. We also discuss several applications of this general theory in formal developments.

Research GroupFoundations of Computing group
Conference5th International Conference on Interactive Theorem Proving
Page range111-127
ISSN0302-9743
ISBN
Hardcover9783319089690
PublisherSpringer
Publication dates
Print2014
Publication process dates
Deposited23 Apr 2015
Output statusPublished
Accepted author manuscript
Copyright Statement

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-08970-6_8

Additional information

Published paper appears in: Interactive Theorem Proving, Volume 8558 of the series Lecture Notes in Computer Science pp 111-127, 2014

Web address (URL)http://dx.doi.org/10.1007/978-3-319-08970-6_8
LanguageEnglish
Book titleInteractive Theorem Proving: 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings
Permalink -

https://repository.mdx.ac.uk/item/85116

Log in to edit

Download files

Accepted author manuscript
card.pdf

  • 16
    total views
  • 9
    total downloads
  • 1
    views this month
  • 1
    downloads this month

Export as