Universal Turing Machine and Computability Theory in Isabelle/HOL

Jian Xu, Xingyuan Zhang, Christian Urban, Sebastiaan J. C. Joosten

    Research output: Contribution to journalArticleAcademicpeer-review

    124 Downloads (Pure)


    We formalise results from computability theory: recursive functions, undecidability of the halting problem, and the existence of a universal Turing machine. This formalisation is the AFP entry corresponding to the paper Mechanising Turing Machines and Computability Theory in Isabelle/HOL, ITP 2013.
    Original languageEnglish
    JournalArchive of Formal Proofs
    Publication statusPublished - 1 Feb 2019


    Dive into the research topics of 'Universal Turing Machine and Computability Theory in Isabelle/HOL'. Together they form a unique fingerprint.

    Cite this