Abstract / Description of output
We discuss the formalization, in the Matita Theorem Prover, of basic results on multi-tapes Turing machines, up to the existence of a (certified) Universal Machine, and propose it as a natural benchmark for comparing different interactive provers and assessing the state of the art in the mechanization of formal reasoning. The work is meant to be a preliminary step towards the creation of a formal repository in Complexity Theory, and is a small piece in our long-term Reverse Complexity program, aiming to a comfortable, machine independent axiomatization of the field.
| Original language | English |
|---|---|
| Pages (from-to) | 23-42 |
| Number of pages | 20 |
| Journal | Theoretical Computer Science |
| Volume | 603 |
| Early online date | 14 Jul 2015 |
| DOIs | |
| Publication status | Published - 25 Oct 2015 |
Fingerprint
Dive into the research topics of 'A formalization of multi-tape Turing machines'. Together they form a unique fingerprint.Profiles
-
Wilmer Ricciotti
- School of Informatics - Senior Researcher
- Laboratory for Foundations of Computer Science
- Foundations of Computation
Person: Academic: Research Active (Research Assistant)