Towards Turing computability via coinduction

•We adopt coinductive types in Coq to formalize Turing Machines.•We certify the correctness of concrete Turing Machines.•We prove the undecidability of the halting problem.

We adopt corecursion and coinduction to formalize Turing Machines and their operational semantics in the Coq proof assistant. By combining the formal analysis of converging and diverging computations, via big-step and small-step predicates, our approach allows us to certify the correctness of concrete Turing Machines. An immediate application of our methodology is the proof of the undecidability of the halting problem, therefore our effort may be seen as a first step towards the formal development of basic computability theory.