Mechanised computability theory
Authors
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, publisher = {Springer}, doi = {10.1007/978-3-642-22863-6_22}, month = aug, slides = {http://ts.data61.csiro.au/publications/nicta_slides/4837.pdf}, paperurl = {https://ts.data61.csiro.au/publications/nicta_full_text/4837.pdf}, booktitle = {International Conference on Interactive Theorem Proving}, year = {2011}, editor = {{Marko van Eekeln, Herman Geuvers, Julien Schmaltz, Freek Wiedijk}}, title = {Mechanised Computability Theory}, pages = {297---311}, author = {Norrish, Michael}, address = {Nijmegen, The Netherlands} }