Reseña: Formalizing Turing machines

Se ha publicado un trabajo de razonamiento formalizado con Matita sobre máquinas de Turing titulado Formalizing Turing machines.

Sus autores son Andrea Asperti y Wilmer Ricciotti (de la Universidad de Bolonia, Italia).

Su resumen es

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.

El trabajo se presentó en el WoLLIC 2012 (19th Workshop on Logic, Language, Information and Computation). La transparencias de la presentación se encuentran aquí.