Formalizing Turing Machines

Andrea Asperti, Wilmer Ricciotti

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish
Title of host publicationLogic, Language, Information and Computation
Subtitle of host publication19th International Workshop, WoLLIC 2012, Buenos Aires, Argentina, September 3-6, 2012. Proceedings
PublisherSpringer Berlin Heidelberg
Number of pages25
ISBN (Electronic)978-3-642-32621-9
ISBN (Print)978-3-642-32620-2
Publication statusPublished - 2012

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743

Fingerprint Dive into the research topics of 'Formalizing Turing Machines'. Together they form a unique fingerprint.

Cite this