(*<*)
theory Paper
imports UTM
begin

declare [[show_question_marks = false]]
(*>*)

section {* Introduction *}

text {*

We formalised in earlier work the correctness 
proofs for two algorithms in Isabelle/HOL, one about type-checking in LF and 
another about deciding requests in access control \cite{UrbanCheneyBerghofer11} [???]: 
these 
formalisations 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 for the algorithms. The reason is that both algorithms are formulated
in terms of inductive predicates. Suppose @{text "P"} stands for 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 {* Wang Tiles *}

text {*
  Used in texture mapings - graphics
*}


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
(*>*)