Paper Info
Title
A Coinductive Animation of Turing Machines.
Abstract
We adopt corecursion and coinduction to formalize Turing Machines and their operational semantics in the proof assistant Coq. By combining the formal analysis of converging and diverging evaluations, our approach allows us to certify the implementation of the functions computed by concrete Turing Machines. Our effort may be seen as a first step towards the formal development of basic computability theory.
Year
DOI
Venue
2014
10.1007/978-3-319-15075-8-6
Lecture Notes in Computer Science
Field
DocType
Volume
Programming language,Computer science,Corecursion,Computability theory,Super-recursive algorithm,Theoretical computer science,Coinduction,Turing machine,Turing machine examples,Non-deterministic Turing machine,Proof assistant
Conference
8941
ISSN
Citations 
PageRank 
0302-9743
1
0.39
References 
Authors
10
1
Name
Order
Citations
PageRank
Alberto Ciaffaglione1589.97