A formalization of multi-tape Turing machines
- Submitting institution
-
University of Edinburgh
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 110110781
- Type
- D - Journal article
- DOI
-
10.1016/j.tcs.2015.07.013
- Title of journal
- Theoretical Computer Science
- Article number
- -
- First page
- 23
- Volume
- 603
- Issue
- -
- ISSN
- 0304-3975
- Open access status
- Out of scope for open access requirements
- Month of publication
- July
- Year of publication
- 2015
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
1
- Research group(s)
-
C - Foundations of Computation
- Citation count
- 6
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- It describes the implementation and verification of multi-tape Turing machines in the Matita proof assistant, up to a constructive, direct proof of existence of a certified universal machine. It provides a novel technique to build complex machines through sequencing, conditionals and loops (dispelling the common belief that Turing machines are not compositional), a library of simple machines with straightforward semantics and correctness proofs, and proof principles to reason on complex machines by breaking them down to their basic components. The technique was used in a subsequent verification work on Turing machines (Forster et al., ITP 2018).
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -