Re: [Hol-info] security of proofs in HOL

[Roger B. J. <rb...@rb...>]

On Monday 04 August 2003 12:59 pm, Kai Kapp wrote:

> does anyboy know any publication(s) about the actual security
> of proofs in HOL98 ?

There is some discussion of this kind of question
in Donald MacKenzie's book "Mechanising Proof".

There are specific references to HOL which can
be found through the index, but I think all
the material will relate to predecessors of HOL98.

Specifically in relation to security of proofs
there is discussion of the LCF architecture and
its role in ensuring security, and also of
"mk_thm" (both "LCF" and "mk_thm" are in the index).

Its all informal and lightweight, but the book
is a good read for those interested in the history.

Roger Jones