tm: README@8dde2e46c69d (annotated)

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
174 3674347dd98e tuning Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 173 diff changeset	27
3674347dd98e tuning Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 173 diff changeset	28
3674347dd98e tuning Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 173 diff changeset	29	isabelle make utm -- creates the big session file
3674347dd98e tuning Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 173 diff changeset	30	isabelle make itp -- creates paper

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Tue, 26 Feb 2013 17:39:47 +0000
changeset 200	8dde2e46c69d
parent 174	3674347dd98e
child 237	06a6db387cd2
permissions	-rw-r--r--