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 <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.

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.


	Makarius




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