Formalisation of Turing Machines and Computability Theory+ −
=========================================================+ −
+ −
thys - contains the formalisation+ −
+ −
Turing.thy: Basic definitions of Turing machines.+ −
Turing_Hoare.thy: Contains the Hoare rules + −
Uncomputable.thy: The existence of Turing uncomputable functions+ −
Abacus_Mopup.thy: Mopup TM which is used when compiling Abacus+ −
programs+ −
Abacus.thy: Basic definitions of abacus machines (an intermediate+ −
"language" for compiling recursive functions into + −
Turing machines)+ −
Rec_Def.thy: Basic definitions of recursive functions.+ −
Recursive.thy: The compilation of recursive functions into+ −
abacus machines.+ −
UF.thy: The construction of the Universal Function, named "rec_F" and+ −
the proof of its correctness.+ −
UTM.thy: Obtaining a Universal Turing machine by translating the+ −
Turing machine compiled from "rec_F" with some + −
+ −
+ −
Paper - contains the files for the paper+ −
+ −
Attic - old files+ −
Literature - related work+ −
+ −
+ −
isabelle build -d . UTM+ −
isabelle make utm -- creates the big session file+ −
+ −
isabelle make itp -- creates paper+ −
+ −
+ −
+ −
============================+ −
ROOT setup+ −
+ −
isabelle build -d . Slides2+ −