tm: README@a2707a5652d9 (annotated)

299 a2707a5652d9 test Christian Urban <christian.urban@kcl.ac.uk> parents: 298 diff changeset	1	=========================================================
a2707a5652d9 test Christian Urban <christian.urban@kcl.ac.uk> parents: 298 diff changeset	2	MOST OF THE MATERIAL IS NOW IN THE AFP
a2707a5652d9 test Christian Urban <christian.urban@kcl.ac.uk> parents: 298 diff changeset	3
a2707a5652d9 test Christian Urban <christian.urban@kcl.ac.uk> parents: 298 diff changeset	4
163 67063c5365e1 changed theory names to uppercase Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 128 diff changeset	5	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	6	=========================================================
128 7dc064e64ab2 added readme Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	7
7dc064e64ab2 added readme Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	8	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	9
67063c5365e1 changed theory names to uppercase Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 128 diff changeset	10	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	11	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	12	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	13	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	14	programs
163 67063c5365e1 changed theory names to uppercase Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 128 diff changeset	15	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	16	"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	17	Turing machines)
67063c5365e1 changed theory names to uppercase Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 128 diff changeset	18	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	19	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	20	abacus machines.
67063c5365e1 changed theory names to uppercase Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 128 diff changeset	21	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	22	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	23	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	24	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	25
67063c5365e1 changed theory names to uppercase Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 128 diff changeset	26
128 7dc064e64ab2 added readme Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	27	Paper - contains the files for the paper
7dc064e64ab2 added readme Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	28
7dc064e64ab2 added readme Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	29	Attic - old files
7dc064e64ab2 added readme Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	30	Literature - related work
174 3674347dd98e tuning Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 173 diff changeset	31
3674347dd98e tuning Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 173 diff changeset	32
237 06a6db387cd2 updated and small modification Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 174 diff changeset	33	isabelle build -d . UTM
174 3674347dd98e tuning Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 173 diff changeset	34	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	35
272 42f2c28d1ce6 new verison of the slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	36	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	37
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
42f2c28d1ce6 new verison of the slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	40	============================
42f2c28d1ce6 new verison of the slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	41	ROOT setup
42f2c28d1ce6 new verison of the slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 237 diff changeset	42
298 ac5461882f3e test Christian Urban <christian.urban@kcl.ac.uk> parents: 272 diff changeset	43	isabelle build -d . Slides2
ac5461882f3e test Christian Urban <christian.urban@kcl.ac.uk> parents: 272 diff changeset	44
ac5461882f3e test Christian Urban <christian.urban@kcl.ac.uk> parents: 272 diff changeset	45	============================

author	Christian Urban <christian.urban@kcl.ac.uk>
	Thu, 22 Feb 2024 14:06:37 +0000
changeset 299	a2707a5652d9
parent 298	ac5461882f3e
permissions	-rw-r--r--