Skip to main content


Mechanised computability theory


Michael Norrish


Australian National University


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

    publisher        = {Springer},
    doi              = {10.1007/978-3-642-22863-6_22},
    author           = {Norrish, Michael},
    month            = {aug},
    slides           = {},
    editor           = {{Marko van Eekeln, Herman Geuvers, Julien Schmaltz, Freek Wiedijk}},
    year             = {2011},
    title            = {Mechanised Computability Theory},
    booktitle        = {International Conference on Interactive Theorem Proving},
    pages            = {297–311},
    address          = {Nijmegen, The Netherlands}