A formalization of multi-tape Turing machines
From MaRDI portal
(Redirected from Publication:744986)
interactive theorem provingTuring machinesautomatic verificationuniversal machinecertified correctnessMatita
Recommendations
Cites work
- scientific article; zbMATH DE number 3131080 (Why is no real title available?)
- scientific article; zbMATH DE number 5595151 (Why is no real title available?)
- scientific article; zbMATH DE number 3664335 (Why is no real title available?)
- scientific article; zbMATH DE number 1142308 (Why is no real title available?)
- scientific article; zbMATH DE number 3438370 (Why is no real title available?)
- A bi-directional refinement algorithm for the calculus of (co)inductive constructions
- A formal proof of Borodin-Trakhtenbrot's gap theorem
- A formally verified proof of the prime number theorem
- A list-machine benchmark for mechanized metatheory
- A machine-checked proof of the odd order theorem
- An introduction to small scale reflection in Coq
- Computability and Logic
- Computational Complexity
- Engineering formal metatheory
- Formal certification of a compiler back-end or: programming a compiler with a proof assistant
- Formalizing Turing Machines
- Hints in Unification
- Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics
- Mechanised computability theory
- Mechanising Turing machines and computability theory in Isabelle/HOL
- On Formalisms for Turing Machines
- On the Computational Complexity of Algorithms
- One-tape, off-line Turing machine computations
- Operating system verification---an overview
- Some considerations on the usability of interactive provers
- The Matita interactive theorem prover
- The intensional content of Rice's theorem
- Theorem Proving in Higher Order Logics
- Two-Tape Simulation of Multitape Turing Machines
- Zen and the art of formalisation
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
- scientific article; zbMATH DE number 7167584 (Why is no real title available?)
- 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
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)
