Mechanised Computability Theory

Select |


Norrish, Michael

Norrish, Michael


Conference Material

International Conference on Interactive Theorem Proving

Nijmegen, The Netherlands


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.


Copyright Springer-Verlag.


Norrish, Michael. Mechanised Computability Theory. In: Marko van Eekeln, Herman Geuvers, Julien Schmaltz, Freek Wiedijk Editor, editor/s. International Conference on Interactive Theorem Proving; Nijmegen, The Netherlands. Springer; 2011-08-22. 297–311.

Loading citation data...

Citation counts
(Requires subscription to view)