King's College London

Research portal

Mechanising Turing machines and computability theory in Isabelle/HOL

Research output: Chapter in Book/Report/Conference proceedingConference paper

Jian Xu, Xingyuan Zhang, Christian Urban

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages147-162
Number of pages16
Volume7998 LNCS
DOIs
Publication statusPublished - 2013
Event4th International Conference on Interactive Theorem Proving, ITP 2013 - Rennes, France
Duration: 22 Jul 201326 Jul 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7998 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Conference

Conference4th International Conference on Interactive Theorem Proving, ITP 2013
CountryFrance
CityRennes
Period22/07/201326/07/2013

King's Authors

Abstract

We formalise results from computability theory in the theorem prover Isabelle/HOL. Following the textbook by Boolos et al, we formalise Turing machines and relate them to abacus machines and recursive functions. We "tie the know" between these three computational models by formalising a universal function and obtaining from it a universal Turing machine by our verified translation from recursive functions to abacus programs and from abacus programs to Turing machine programs. Hoare-style reasoning techniques allow us to reason about concrete Turing machine and abacus programs.

View graph of relations

© 2018 King's College London | Strand | London WC2R 2LS | England | United Kingdom | Tel +44 (0)20 7836 5454