Universal Turing Machine and Computability Theory in Isabelle/HOL

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

Universal Turing Machine and Computability Theory in Isabelle/HOL

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

Research output: Contribution to journal › Article › Academic › peer-review

124 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 language	English
Journal	Archive of Formal Proofs
Publication status	Published - 1 Feb 2019

Access to Document

universalAccepted author version, 1.27 MB

https://www.isa-afp.org/entries/Universal_Turing_Machine.html

Cite this

@article{4749c6d7dead480da57e55a83d6900f6,

title = "Universal Turing Machine and Computability Theory in Isabelle/HOL",

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.",

author = "Jian Xu and Xingyuan Zhang and Christian Urban and Joosten, {Sebastiaan J. C.}",

note = "http://isa-afp.org/entries/Universal_Turing_Machine.html, Formal proof development",

year = "2019",

month = feb,

day = "1",

language = "English",

journal = "Archive of Formal Proofs",

issn = "2150-914x",

publisher = "SourceForge",

}

TY - JOUR

T1 - Universal Turing Machine and Computability Theory in Isabelle/HOL

AU - Xu, Jian

AU - Zhang, Xingyuan

AU - Urban, Christian

AU - Joosten, Sebastiaan J. C.

N1 - http://isa-afp.org/entries/Universal_Turing_Machine.html, Formal proof development

PY - 2019/2/1

Y1 - 2019/2/1

N2 - 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.

AB - 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.

M3 - Article

JO - Archive of Formal Proofs

JF - Archive of Formal Proofs

SN - 2150-914x

ER -

Universal Turing Machine and Computability Theory in Isabelle/HOL

Abstract

Access to Document

Fingerprint

Cite this