(*<*)

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

(*>*)