Re: [isabelle] Isabelle Foundation & Certification

On Sun, 20 Sep 2015, Chantal Keller wrote:

As far as I am aware, the more convincing attempt at checking proofs coming from provers of the HOL community is Holide <>. 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.

That is definitely interesting work. I had some discussions about it with Ali Assaf in October 2013, IIRC.

What is also remarkable in the above paper: the "HOL family" only covers the actual HOL systems, while Isabelle/HOL falls into the category of "other systems" (like Coq, Nuprl).

Thus the HOL family proper is defined as the systems with full import/export wrt. OpenTheory.


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