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 paperAttic - old filesLiterature - related workisabelle build -d . UTMisabelle make utm -- creates the big session fileisabelle make itp -- creates paper============================ROOT setupisabelle build -d . Slides2