diff -r bb0b6d818e99 -r 50880fcda34d Paper.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper.thy	Sat Dec 29 20:17:57 2012 +0000
@@ -0,0 +1,72 @@
+(*<*)
+theory Paper
+imports UTM
+begin
+
+declare [[show_question_marks = false]]
+(*>*)
+
+section {* Introduction *}
+
+text {*
+
+In earlier work, we formalised in Isabelle/HOL the correctness 
+proofs for two algorithms, one about type-checking in LF and 
+another about deciding requests in access control [???]. These 
+formalisation efforts uncovered a gap in the informal correctness 
+proof of the former and made us realise that important details 
+were left out in the informal model for the latter. However, 
+in both cases we were unable to formalise computablility 
+arguments. The reason is that both algorithms are formulated
+as inductive predicates. Say @{text "P"} is one such predicate.
+Decidability of @{text P} usually amounts to showing whether 
+@{term "P \<or> \<not>P"} holds. But this does not work in Isabelle/HOL,
+since it is a theorem prover based on classical logic where
+the law of excluded midle ensures that @{term "P \<or> \<not>P"} is 
+always provable.   
+
+
+
+
+These algorithms
+were given as inductively defined predicates.  
+inductively defined predicates, but 
+
+
+Norrish choose the $\lambda$-calculus as a starting point
+for his formalisation, because of its ``simplicity'' [Norrish]
+ 
+``Turing machines are an even more daunting prospect'' [Norrish]
+
+
+Our formalisation follows XXX
+
+\noindent
+{\bf Contributions:} 
+
+*}
+
+section {* Related Work *}
+
+text {*
+  The most closely related work is by Norrish. He bases his approach on 
+  lambda-terms. For this he introduced a clever rewriting technology
+  based on combinators and de-Bruijn indices for
+  rewriting modulo $\beta$-equivalence (to keep it manageable)
+*}
+
+
+(*
+Questions:
+
+Can this be done: Ackerman function is not primitive 
+recursive (Nora Szasz)
+
+Tape is represented as two lists (finite - usually infinite tape)?
+
+*)
+
+
+(*<*)
+end
+(*>*)
\ No newline at end of file