8 |
8 |
9 section {* Introduction *} |
9 section {* Introduction *} |
10 |
10 |
11 text {* |
11 text {* |
12 |
12 |
13 In earlier work, we formalised in Isabelle/HOL the correctness |
13 We formalised in earlier work the correctness |
14 proofs for two algorithms, one about type-checking in LF and |
14 proofs for two algorithms in Isabelle/HOL, one about type-checking in LF and |
15 another about deciding requests in access control [???]. These |
15 another about deciding requests in access control \cite{UrbanCheneyBerghofer11} [???]: |
16 formalisation efforts uncovered a gap in the informal correctness |
16 these |
|
17 formalisations uncovered a gap in the informal correctness |
17 proof of the former and made us realise that important details |
18 proof of the former and made us realise that important details |
18 were left out in the informal model for the latter. However, |
19 were left out in the informal model for the latter. However, |
19 in both cases we were unable to formalise computablility |
20 in both cases we were unable to formalise computablility |
20 arguments. The reason is that both algorithms are formulated |
21 arguments for the algorithms. The reason is that both algorithms are formulated |
21 as inductive predicates. Say @{text "P"} is one such predicate. |
22 in terms of inductive predicates. Suppose @{text "P"} stands for one such predicate. |
22 Decidability of @{text P} usually amounts to showing whether |
23 Decidability of @{text P} usually amounts to showing whether |
23 @{term "P \<or> \<not>P"} holds. But this does not work in Isabelle/HOL, |
24 @{term "P \<or> \<not>P"} holds. But this does not work in Isabelle/HOL, |
24 since it is a theorem prover based on classical logic where |
25 since it is a theorem prover based on classical logic where |
25 the law of excluded midle ensures that @{term "P \<or> \<not>P"} is |
26 the law of excluded midle ensures that @{term "P \<or> \<not>P"} is |
26 always provable. |
27 always provable. |