Re: [isabelle] Isabelle Foundation & Certification


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.


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