Re: [isabelle] Isabelle Foundation & Certification



Dear Ramana,

As far as I am aware, the more convincing attempt at checking proofs
coming from provers of the HOL community is Holide
<https://who.rocq.inria.fr/Ali.Assaf/research/translating-hollight-dedukti-pxtp-2015.pdf>.
It is still costly though, both to produce proofs and check them, but
this cost has been reduced a lot these last years compared to previous
work. It is based on OpenTheory.

I do not know how it compares to the work David mentioned on seL4.

Best,
Chantal.




Le 17/09/2015 12:59, Ramana Kumar a Ãcrit :
Thanks Tjark.

I am aware of Stefan's excellent work, and I'm sorry if I gave the
impression that my proposal was novel in any sense. (Perhaps the part about
verifying the checker is new, but that's just icing for the purposes of
this discussion.)

My concern is whether the proof checker for proof terms is actually used or
not. In an ideal world, I would think that for any substantial
formalisation, the proof terms would be the bulk of the evidence provided
to the certification authority or any other party interested to know why
the claims being made are true, and those proof terms would be checked
regularly (say twice a year) by a small checker if the formalisation is
under continued development. Does anyone actually do that? Is scalability
the only issue?

Apologies if this is veering too far from the original topic. I'm happy to
continue discussion on another thread if desired.

On 17 September 2015 at 20:40, Tjark Weber <tjark.weber at it.uu.se> wrote:

Ramana,

On Thu, 2015-09-17 at 08:38 +1000, Ramana Kumar wrote:
Furthermore, if there is enough community interest, I would be interested
in building a verified proof-checker for Isabelle/HOL. One crucial
ingredient required from the Isabelle community here is the ability to
export proofs in a low-level format (ideally OpenTheory, rather than some
other new format), but I believe you're already quite close to that with
the option to produce proof terms.

Take a look at Stefan Berghofer's thesis. He already implemented a
proof checker for his proof terms (albeit not verified).

The main issue, if I recall correctly, was that these proof terms could
become huge.

Best,
Tjark








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.