Turing machines build the traditional foundation of the theory of computation and complexity. However, concrete Turing machines are often only sketched out. Even if authors define the complete machine, they leave the invariants to figure out for the reader. Moreover, it is common to employ the Church-Turing thesis, to (informally) conclude that a function is Turing-computable. Reasons for that are manifold. Turing machines are very low-level, because the operations on tapes are primitive. They are also non-compositional; control-flow operators like sequential composition and loops are not available. Reasoning about invariants and concrete machine states is tedious, because the execution of the machine could proceed from one state of the machine to any other state; the set of states may also be huge for complex machines.
In this thesis, we fill these gaps. We present a framework developed in the theorem prover Coq, in that we can define, specify, and formally verify multi-tape Turing machines. The framework eases programming and verification of Turing machines, because it provides abstractions like values and control-flow operators. We showcase the power of this framework by programming and verifying a multi-tape Turing machine that simulates a two-stack machine for the call-by-value λ-calculus.
| [1] | Andrea Asperti and Wilmer Ricciotti. Formalizing Turing Machines. In Logic, Language, Information and Computation, pages 1--25. Springer, 2012. |
| [2] | Andrea Asperti and Wilmer Ricciotti. A formalization of multi-tape Turing machines. Theoretical Computer Science, 603:23--42, 2015. |
| [3] | Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi. The Matita Interactive Theorem Prover. In International Conference on Automated Deduction, pages 64--69. Springer, 2011. |
| [4] | George S Boolos, John P Burgess, and Richard C Jeffrey. Computability and Logic. 5th, 2007. |
| [5] | Pierre Castéran and Matthieu Sozeau. A Gentle Introduction to Type Classes and Relations in Coq. Technical report, Technical Report hal-00702455, version 1, 2012. |
| [6] | Alberto Ciaffaglione. Towards Turing computability via coinduction. Science of Computer Programming, 126:31--51, 2016. |
| [7] | Edsger W Dijkstra. Go to Statement Considered Harmful. In Software pioneers, pages 351--355. Springer, 2002. |
| [8] | Yannick Forster, Edith Heiter, and Gert Smolka. Verification of PCP-Related Computational Reductions in Coq. In International Conference on Interactive Theorem Proving, pages 253--269. Springer, 2018. |
| [9] | Yannick Forster and Fabian Kunze. Verified extraction from coq to a lambda-calculus. In Coq Workshop, volume 2016, 2016. |
| [10] | Yannick Forster, Fabian Kunze, and Marc Roth. The strong invariance thesis for a λ-calculus. LOLA workshop 2017, Reykjavik, Iceland, 2017. [ .pdf ] |
| [11] | Yannick Forster and Dominique Larchey-Wendling. Towards a library of formalised undecidable problems in Coq: The undecidability of intuitionistic linear logic. LOLA workshop 2018, Oxford, UK, 2018. [ .pdf ] |
| [12] | Yannick Forster and Gert Smolka. Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq. In International Conference on Interactive Theorem Proving, pages 189--206. Springer, 2017. |
| [13] | Fabian Kunze, Gert Smolka, and Yannick Forster. Formal Small-step Verification of a Call-by-value Lambda Calculus Machine. Technical report, arxiv 1806.03205, Jun 2018. |
| [14] | Jan Christian Menz. A Coq Library for Finite Types. Bachelor's thesis, Universität des Saarlandes, 2016. [ http ] |
| [15] | Michael Norrish. Mechanised computability theory. In International Conference on Interactive Theorem Proving, pages 297--311. Springer, 2011. |
| [16] | The Coq Proof Assistant. http://coq.inria.fr. |
| [17] | Jian Xu, Xingyuan Zhang, and Christian Urban. Mechanising Turing machines and computability theory in Isabelle/HOL. In International Conference on Interactive Theorem Proving, pages 147--162. Springer, 2013. |