Reseña: Mechanising Turing machines and computability theory in Isabelle/HOL

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre modelos de computación titulado Mechanising Turing machines and computability theory in Isabelle/HOL.

Sus autores son Jian Xu, Xingyuan Zhang y Christian Urban.

Su resumen es

We present a formalised theory of computability in the theorem prover Isabelle/HOL. This theorem prover is based on classical logic which precludes direct reasoning about computability: every boolean predicate is either true or false because of the law of excluded middle. The only way to reason about computability in a classical theorem prover is to formalise a concrete model of computation. We formalise Turing machines and relate them to abacus machines and recursive functions. We also formalise a universal Turing machine and Hoare-style reasoning techniques that allow us to reason about Turing machine programs. Our theory can be used to formalise other computability results.

Las teorías desarrolladas en Isabelle/HOL se encuentran en aquí.