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 |

Authors (1 rows)

Cited by (2 rows)

References (6 rows)

Name | Order | Citations | PageRank |
---|---|---|---|

Alberto Ciaffaglione | 1 | 58 | 9.97 |