Skip to main content

TS

Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁

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,
    publisher        = {Springer},
    author           = {Norrish, Michael and Huffman, Brian},
    month            = jul,
    slides           = {http://ts.data61.csiro.au/publications/nicta_slides/6676.pdf},
    editor           = {{Sandrine Blazy and Christine Paulin-Mohring and David Pichardie}},
    year             = {2013},
    title            = {Ordinals in {HOL}: Transfinite Arithmetic up to (and beyond) ω₁},
    booktitle        = {International Conference on Interactive Theorem Proving},
    pages            = {133-146},
    address          = {Rennes, France}
  }

Download

Served by Apache on Linux on seL4.