Towards Turing computability via coinduction

Asperti, 2012, Formalizing Turing Machines, vol. 7456, 1 Boolos, 2007 Ciaffaglione, 2011, A coinductive semantics of the unlimited register machine, vol. 73, 49 Ciaffaglione, 2014, A coinductive animation of Turing Machines, vol. 8941, 80 Ciaffaglione Coquand, 1993, Infinite objects in type theory, vol. 806, 62 Giménez, 1994, Codifying guarded definitions with recursive schemes, vol. 996, 39 Cutland, 1980 Hur, 2013, The power of parameterization in coinductive proof, 193 Leroy, 2006, Coinductive big-step operational semantics, vol. 3924, 54 Norrish, 2011, Mechanised computability theory, vol. 6898, 297 Turing, 1936, On computable numbers, with an application to the Entscheidungsproblem Xu, 2013, Mechanising Turing Machines and computability theory in Isabelle/HOL, vol. 7998, 147 The Coq Development Team