tm: README@6836da75b3ac (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
237 06a6db387cd2 updated and small modification Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 174 diff changeset	29	isabelle build -d . UTM
174 3674347dd98e tuning Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 173 diff changeset	30	isabelle make utm -- creates the big session file
237 06a6db387cd2 updated and small modification Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 174 diff changeset	31
272 42f2c28d1ce6 new verison of the slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	32	isabelle make itp -- creates paper
42f2c28d1ce6 new verison of the slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	33
42f2c28d1ce6 new verison of the slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	34
42f2c28d1ce6 new verison of the slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	35
42f2c28d1ce6 new verison of the slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	36	============================
42f2c28d1ce6 new verison of the slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	37	ROOT setup
42f2c28d1ce6 new verison of the slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	38
42f2c28d1ce6 new verison of the slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	39	isabelle build -d . Slides2

author	Christian Urban <urbanc@in.tum.de>
	Thu, 10 Jan 2019 12:51:24 +0000
changeset 294	6836da75b3ac
parent 272	42f2c28d1ce6
child 298	ac5461882f3e
permissions	-rw-r--r--