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

    58 Downloads (Pure)

    Abstract

    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

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

  • Cite this

    Xu, J., Zhang, X., Urban, C., & Joosten, S. J. C. (2019). Universal Turing Machine and Computability Theory in Isabelle/HOL. Archive of Formal Proofs.