A coinductive animation of Turing Machines
Alberto Ciaffaglione
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].
Last updated: October 31, 2014