A formalization of multi-tape Turing machines

DOI10.1016/j.tcs.2015.07.013zbMath1330.68065OpenAlexW2118758698WikidataQ56112363 ScholiaQ56112363MaRDI QIDQ744986

Andrea Asperti, Wilmer Ricciotti

Publication date: 12 October 2015

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2015.07.013

zbMATH Keywords

Turing machinesautomatic verificationinteractive theorem provinguniversal machinecertified correctnessMatita

Mathematics Subject Classification ID

Related Items

Reverse complexity ⋮ Weak call-by-value lambda calculus as a model of computation in Coq ⋮ Constructive Many-one Reduction from the Halting Problem to Semi-unification (Extended Version) ⋮ Call-by-value lambda calculus as a model of computation in Coq

Uses Software

• Matita
• Coq/SSReflect
• PoplMark

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics
• Operating system verification---an overview
• A list-machine benchmark for mechanized metatheory
• A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions
• Formalizing Turing Machines
• A Formal Proof of Borodin-Trakhtenbrot’s Gap Theorem
• Mechanised Computability Theory
• Zen and the art of formalisation
• Hints in Unification
• Engineering formal metatheory
• The intensional content of Rice's theorem
• Computability and Logic
• Some Considerations on the Usability of Interactive Provers
• The Matita Interactive Theorem Prover
• A formally verified proof of the prime number theorem
• Computational Complexity
• Mechanising Turing Machines and Computability Theory in Isabelle/HOL
• A Machine-Checked Proof of the Odd Order Theorem
• On the Computational Complexity of Algorithms
• Formal certification of a compiler back-end or
• Theorem Proving in Higher Order Logics
• Two-Tape Simulation of Multitape Turing Machines
• On Formalisms for Turing Machines
• One-tape, off-line Turing machine computations