Abstract
We formalise results from computability theory: recursive functions,
undecidability of the halting problem, and the existence of a
universal Turing machine. This formalisation is the AFP entry
corresponding to the paper Mechanising Turing Machines and Computability Theory
in Isabelle/HOL, ITP 2013.
BSD LicenseTopics
Theories of Universal_Turing_Machine
- Turing
- Turing_Hoare
- Uncomputable
- Abacus_Mopup
- Abacus
- Abacus_Defs
- Rec_Def
- Abacus_Hoare
- Recursive
- Recs
- UF
- UTM