Paper Info
Title
Towards Turing computability via coinduction.
Abstract
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. 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.
Year
DOI
Venue
2016
10.1016/j.scico.2016.02.004
Sci. Comput. Program.
Keywords
Field
DocType
Program certification,Coq proof assistant,Coinductive types
Programming language,Turing completeness,Hyperarithmetical theory,Computer science,Super-recursive algorithm,Theoretical computer science,Turing machine,Description number,Turing reduction,Turing,Halting problem
Journal
Volume
Issue
ISSN
126
C
0167-6423
Citations 
PageRank 
References 
2
0.40
6
Authors
1
Name
Order
Citations
PageRank
Alberto Ciaffaglione1589.97