We discuss the formalization, in the Matita Theorem Prover, of a few, basic results on Turing Machines, up to the existence of a (certified) Universal Machine. 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 Reverse Complexity program, aiming to a comfortable, machine independent axiomatization of the field.
Formalizing Turing Machines / A.Asperti; W.Ricciotti. - STAMPA. - 7456:(2012), pp. 1-25. (Intervento presentato al convegno Logic, Language, Information and Computation - 19th International Workshop, WoLLIC 2012 tenutosi a Buenos Aires, Argentina nel 3-6 September 2012) [10.1007/978-3-642-32621-9_1].
Formalizing Turing Machines
ASPERTI, ANDREA;RICCIOTTI, WILMER
2012
Abstract
We discuss the formalization, in the Matita Theorem Prover, of a few, basic results on Turing Machines, up to the existence of a (certified) Universal Machine. 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 Reverse Complexity program, aiming to a comfortable, machine independent axiomatization of the field.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.