A coinductive animation of Turing Machines

We formalize Turing Machines (TMs) and their operational semantics via (co)inductive types in Coq:

• the tape is encoded by a pair of streams (a zipper), managed by corecursion;
• the operational semantics is modeled through two big-step predicates:
  • an inductive one for converging evaluations
  • a coinductive one for diverging evaluations
• such a machinery allows us to address the certification of concrete TMs.

Our research has been published at SBMF 2014, and the Coq script is available [here].