[opentheory-users] Scalable LCF-style proof translation

[Ramana Kumar]

Cezary Kaliszyk and Alexander Krauss have done a lovely piece of work that
was just presented at ITP 2013 (
http://cl-informatik.uibk.ac.at/users/cek/docs/kaliszyk-itp13.pdf) about
efficient import from HOL Light into Isabelle/HOL.

Their approach has many similarities to OpenTheory, and their proof trace
format is not too different from OpenTheory article format, and indeed in
Alex's talk he said integration with OpenTheory would be a worthy goal.

The performance of their method is very impressive, and certainly faster
than using OpenTheory as it is now, so I think it would greatly benefit
OpenTheory to adopt and standardise K&K's ideas.

I write this message to ask OpenTheory users for their comments on this
proposal, and to make a call for volunteers to help with the
integration/adoption. As a first step, perhaps we could just make a list of
the differences from how OpenTheory currently works, to see what needs to
be done.

Ramana
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20130723/48a2cb00/attachment.html>