Trustworthy Systems

Mechanised computability theory

Authors

Michael Norrish

NICTA\ Australian National University

Abstract

This paper presents a mechanisation of some basic computability theory. The mechanisation uses two models: the recursive functions and the lambda-calculus, and shows that they have equivalent computational power. Results proved include the Recursion Theorem, an instance of the s-m-n theorem, the existence of a universal machine, Rice's Theorem, and closure facts about the recursive and recursively enumerable sets. The mechanisation was performed in the HOL4 system and is available online.

BibTeX Entry

  @inproceedings{Norrish_11,
    address          = {Nijmegen, The Netherlands},
    author           = {Norrish, Michael},
    booktitle        = {International Conference on Interactive Theorem Proving},
    doi              = {10.1007/978-3-642-22863-6_22},
    editor           = {{Marko van Eekeln, Herman Geuvers, Julien Schmaltz, Freek Wiedijk}},
    month            = aug,
    pages            = {297---311},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/4837.pdf},
    publisher        = {Springer},
    slides           = {https://trustworthy.systems/publications/nicta_slides/4837.pdf},
    title            = {Mechanised Computability Theory},
    year             = {2011}
  }

Download