TY - GEN
T1 - Mechanised computability theory
AU - Norrish, Michael
PY - 2011
Y1 - 2011
N2 - This paper presents a mechanisation of some basic computability theory. The mechanisation uses two models: the recursive functions and the λ-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.
AB - This paper presents a mechanisation of some basic computability theory. The mechanisation uses two models: the recursive functions and the λ-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.
UR - http://www.scopus.com/inward/record.url?scp=80052147502&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-22863-6_22
DO - 10.1007/978-3-642-22863-6_22
M3 - Conference contribution
SN - 9783642228629
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 297
EP - 311
BT - Interactive Theorem Proving - Second International Conference, ITP 2011, Proceedings
T2 - 2nd International Conference on Interactive Theorem Proving, ITP 2011
Y2 - 22 August 2011 through 25 August 2011
ER -