Mechanising Turing Machines and Computability Theory in Isabelle/HOL

DOI10.1007/978-3-642-39634-2_13zbMath1317.68237OpenAlexW50191166MaRDI QIDQ5327342

Christian Urban, Jian Xu, Xing-Yuan Zhang

Publication date: 7 August 2013

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-39634-2_13

Mathematics Subject Classification ID

Related Items (10)

Reverse complexity ⋮ Formalisation vs. Understanding ⋮ Weak call-by-value lambda calculus as a model of computation in Coq ⋮ Typing total recursive functions in Coq ⋮ The DPRM Theorem in Isabelle (Short Paper). ⋮ Unnamed Item ⋮ A Coinductive Animation of Turing Machines ⋮ A formalization of multi-tape Turing machines ⋮ Incompleteness, Undecidability and Automated Proofs ⋮ Call-by-value lambda calculus as a model of computation in Coq

Uses Software

• Unnamed Item

This page was built for publication: Mechanising Turing Machines and Computability Theory in Isabelle/HOL