163
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
1 |
Formalisation of Turing Machines and Computability Theory
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
2 |
=========================================================
|
128
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
3 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
4 |
thys - contains the formalisation
|
163
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
5 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
6 |
Turing.thy: Basic definitions of Turing machines.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
7 |
Turing_Hoare.thy: Contains the Hoare rules
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
8 |
Uncomputable.thy: The existence of Turing uncomputable functions
|
173
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
9 |
Abacus_Mopup.thy: Mopup TM which is used when compiling Abacus
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
10 |
programs
|
163
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
11 |
Abacus.thy: Basic definitions of abacus machines (an intermediate
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
12 |
"language" for compiling recursive functions into
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
13 |
Turing machines)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
14 |
Rec_Def.thy: Basic definitions of recursive functions.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
15 |
Recursive.thy: The compilation of recursive functions into
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
16 |
abacus machines.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
17 |
UF.thy: The construction of the Universal Function, named "rec_F" and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
18 |
the proof of its correctness.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
19 |
UTM.thy: Obtaining a Universal Turing machine by translating the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
20 |
Turing machine compiled from "rec_F" with some
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
21 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
22 |
|
128
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
23 |
Paper - contains the files for the paper
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
24 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
25 |
Attic - old files
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
26 |
Literature - related work
|
174
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
27 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
28 |
|
237
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
29 |
isabelle build -d . UTM
|
174
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
30 |
isabelle make utm -- creates the big session file
|
237
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
31 |
|
174
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
32 |
isabelle make itp -- creates paper |