Mechanising Turing machines and computability theory in Isabelle/HOL

DOI10.1007/978-3-642-39634-2_13MaRDI QIDQ5327342zbMATH OpenOpenAlexFDO

Authors Jian Xu, Christian Urban, Xingyuan 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

Recommendations

• Mechanised computability theory
• Formalizing Turing Machines
• A formalization of multi-tape Turing machines
• A Coinductive Animation of Turing Machines
• Proof pearl: proving a simple von Neumann machine Turing complete

Cited in

(17)

• Weak call-by-value lambda calculus as a model of computation in Coq
• Typing total recursive functions in Coq
• Formalization of the computational theory of a Turing complete functional language model
• Call-by-value lambda calculus as a model of computation in Coq
• Using Isabelle/HOL to verify first-order relativity theory
• A Coinductive Animation of Turing Machines
• Incompleteness, Undecidability and Automated Proofs
• Reverse complexity
• Proof pearl: proving a simple von Neumann machine Turing complete
• Formalizing Turing Machines
• Formalisation vs. understanding. A case study in Isabelle
• Mechanised computability theory
• scientific article; zbMATH DE number 7566048 (Why is no real title available?)
• The DPRM Theorem in Isabelle (Short Paper).
• A mechanisation of computability theory in HOL
• Imperative process algebra and models of parallel computation
• A formalization of multi-tape Turing machines

Describes a project that uses

Uses Software

• Isabelle/HOL

This page was built for publication: Mechanising Turing machines and computability theory in Isabelle/HOL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5327342)