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