Mechanised Computability Theory

Select |




Print


Norrish, Michael

Norrish, Michael


2011-08-22


Conference Material


International Conference on Interactive Theorem Proving


Nijmegen, The Netherlands


297–311


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.


Springer


https://doi.org/10.1007/978-3-642-22863-6_22


http://itp2011.cs.ru.nl/ITP2011/Home.html


Copyright Springer-Verlag. http://springerlink.com


nicta:4837


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. https://doi.org/10.1007/978-3-642-22863-6_22



Loading citation data...

Citation counts
(Requires subscription to view)