A formalization of multi-tape Turing machines
From MaRDI portal
Publication:744986
DOI10.1016/J.TCS.2015.07.013zbMATH Open1330.68065DBLPjournals/tcs/AspertiR15OpenAlexW2118758698WikidataQ56112363 ScholiaQ56112363MaRDI QIDQ744986FDOQ744986
Authors: 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
Recommendations
interactive theorem provingTuring machinesautomatic verificationuniversal machinecertified correctnessMatita
Cites Work
- The Matita interactive theorem prover
- Theorem Proving in Higher Order Logics
- Title not available (Why is that?)
- Computational Complexity
- On the Computational Complexity of Algorithms
- Title not available (Why is that?)
- Formalizing Turing Machines
- A formal proof of Borodin-Trakhtenbrot's gap theorem
- An introduction to small scale reflection in Coq
- The intensional content of Rice's theorem
- Title not available (Why is that?)
- Title not available (Why is that?)
- A formally verified proof of the prime number theorem
- Mechanising Turing machines and computability theory in Isabelle/HOL
- Title not available (Why is that?)
- Computability and Logic
- Two-Tape Simulation of Multitape Turing Machines
- Engineering formal metatheory
- Formal certification of a compiler back-end or: programming a compiler with a proof assistant
- Operating system verification---an overview
- A machine-checked proof of the odd order theorem
- One-tape, off-line Turing machine computations
- A list-machine benchmark for mechanized metatheory
- A bi-directional refinement algorithm for the calculus of (co)inductive constructions
- Mechanised computability theory
- Zen and the art of formalisation
- Hints in Unification
- Some considerations on the usability of interactive provers
- On Formalisms for Turing Machines
- Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics
Cited In (9)
- 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)
- Modeling multitape Minsky and Turing machines by three-tape Minsky machines
- Imperative process algebra and models of parallel computation
- Reverse complexity
- Title not available (Why is that?)
- Mechanising Turing machines and computability theory in Isabelle/HOL
- Formalizing Turing Machines
- Weak call-by-value lambda calculus as a model of computation in Coq
Uses Software
This page was built for publication: A formalization of multi-tape Turing machines
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q744986)
