| author | Christian Urban <christian dot urban at kcl dot ac dot uk> |
| Fri, 15 Feb 2013 14:05:26 +0000 | |
| changeset 173 | b51cb9aef3ae |
| parent 163 | 67063c5365e1 |
| child 174 | 3674347dd98e |
| permissions | -rw-r--r-- |
|
163
67063c5365e1
changed theory names to uppercase
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
128
diff
changeset
|
1 |
Formalisation of Turing Machines and Computability Theory |
|
67063c5365e1
changed theory names to uppercase
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
128
diff
changeset
|
2 |
========================================================= |
|
128
7dc064e64ab2
added readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
3 |
|
|
7dc064e64ab2
added readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
4 |
thys - contains the formalisation |
|
163
67063c5365e1
changed theory names to uppercase
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
128
diff
changeset
|
5 |
|
|
67063c5365e1
changed theory names to uppercase
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
128
diff
changeset
|
6 |
Turing.thy: Basic definitions of Turing machines. |
|
67063c5365e1
changed theory names to uppercase
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
128
diff
changeset
|
7 |
Turing_Hoare.thy: Contains the Hoare rules |
|
67063c5365e1
changed theory names to uppercase
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
128
diff
changeset
|
8 |
Uncomputable.thy: The existence of Turing uncomputable functions |
|
173
b51cb9aef3ae
split Mopup TM into a separate file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
163
diff
changeset
|
9 |
Abacus_Mopup.thy: Mopup TM which is used when compiling Abacus |
|
b51cb9aef3ae
split Mopup TM into a separate file
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
163
diff
changeset
|
10 |
programs |
|
163
67063c5365e1
changed theory names to uppercase
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
128
diff
changeset
|
11 |
Abacus.thy: Basic definitions of abacus machines (an intermediate |
|
67063c5365e1
changed theory names to uppercase
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
128
diff
changeset
|
12 |
"language" for compiling recursive functions into |
|
67063c5365e1
changed theory names to uppercase
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
128
diff
changeset
|
13 |
Turing machines) |
|
67063c5365e1
changed theory names to uppercase
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
128
diff
changeset
|
14 |
Rec_Def.thy: Basic definitions of recursive functions. |
|
67063c5365e1
changed theory names to uppercase
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
128
diff
changeset
|
15 |
Recursive.thy: The compilation of recursive functions into |
|
67063c5365e1
changed theory names to uppercase
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
128
diff
changeset
|
16 |
abacus machines. |
|
67063c5365e1
changed theory names to uppercase
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
128
diff
changeset
|
17 |
UF.thy: The construction of the Universal Function, named "rec_F" and |
|
67063c5365e1
changed theory names to uppercase
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
128
diff
changeset
|
18 |
the proof of its correctness. |
|
67063c5365e1
changed theory names to uppercase
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
128
diff
changeset
|
19 |
UTM.thy: Obtaining a Universal Turing machine by translating the |
|
67063c5365e1
changed theory names to uppercase
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
128
diff
changeset
|
20 |
Turing machine compiled from "rec_F" with some |
|
67063c5365e1
changed theory names to uppercase
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
128
diff
changeset
|
21 |
|
|
67063c5365e1
changed theory names to uppercase
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
128
diff
changeset
|
22 |
|
|
128
7dc064e64ab2
added readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
23 |
Paper - contains the files for the paper |
|
7dc064e64ab2
added readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
24 |
|
|
7dc064e64ab2
added readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
25 |
Attic - old files |
|
7dc064e64ab2
added readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
26 |
Literature - related work |