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

21 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

Computability Theory
Turing Machine
Halting Problem
Recursive Functions
Undecidability
Formalization

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 = "2",
day = "1",
language = "English",
journal = "Archive of Formal Proofs",
issn = "2150-914x",
publisher = "SourceForge",

}

Universal Turing Machine and Computability Theory in Isabelle/HOL. / Xu, Jian; Zhang, Xingyuan; Urban, Christian; Joosten, Sebastiaan J. C.

In: Archive of Formal Proofs, 01.02.2019.

Research output: Contribution to journalArticleAcademicpeer-review

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 -