Trustworthy Systems

Ordinals in HOL: Transfinite arithmetic up to (and beyond) $\omega_1$

Authors

Michael Norrish and Brian Huffman

NICTA

Australian National University

Galois
Inc.

Abstract

We describe a comprehensive HOL mechanisation of the theory of ordinal numbers, focusing on the basic arithmetic operations. Mechanised results include the existence of fixpoints such as ε₀, the existence of normal forms, and the validation of some of the algorithms used in the ACL2 theorem-proving system.

BibTeX Entry

  @inproceedings{Norrish_Huffman_13,
    address          = {Rennes, France},
    author           = {Norrish, Michael and Huffman, Brian},
    booktitle        = {International Conference on Interactive Theorem Proving},
    editor           = {{Sandrine Blazy and Christine Paulin-Mohring and David Pichardie}},
    month            = jul,
    pages            = {133--146},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/6676.pdf},
    publisher        = {Springer},
    slides           = {https://trustworthy.systems/publications/nicta_slides/6676.pdf},
    title            = {Ordinals in {HOL}: Transfinite Arithmetic up to (and beyond) $\omega_1$},
    year             = {2013}
  }

Download