<div dir="ltr"><div><div><div><div><div>So, the first observation is a difference in the article formats:<br><br>Currently, OpenTheory articles are programs for a virtual stack machine.<br></div><div>Stack objects may live inside the dictionary and be referenced (by an explicit ref command) by integer keys, or they can be used directly without going into the dictionary.<br>

</div><div><br>By contrast, K&K articles are programs for a virtual machines without a stack.<br></div>The arguments to commands are given inline with the commands, and are always integer keys (i.e., every object is in the dictionary) or literal names.<br>

<br></div>This simplifies and shortens the article format and processing. There are fewer kinds of object (just terms, types, theorems, and names; whereas OpenTheory also requires numbers and lists) and no stack manipulation commands.<br>

</div><br>(Also, I suspect K&K constants are identical if they have the same name; they aren't generative (identity depends on construction provenance) as in OT. This is more intuitive to my taste.)<br><br></div>
Is there a good reason for the stack-based approach? I couldn't think of any, but maybe I'm missing something.<br>
</div>One thing the stack gives you is the ability to share sub-objects like lists of terms; but I don't think this is worthwhile. (With K&K you of course can still share the main objects (terms,types,thms).)<br>
</div>
<div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Jul 23, 2013 at 11:37 AM, Ramana Kumar <span dir="ltr"><<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" target="_blank">Ramana.Kumar@cl.cam.ac.uk</a>></span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div>Cezary Kaliszyk and Alexander Krauss have done a lovely piece of work that was just presented at ITP 2013 (<a href="http://cl-informatik.uibk.ac.at/users/cek/docs/kaliszyk-itp13.pdf" target="_blank">http://cl-informatik.uibk.ac.at/users/cek/docs/kaliszyk-itp13.pdf</a>) about efficient import from HOL Light into Isabelle/HOL.<br>


<br></div>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.<br>


<br></div>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.<br><br>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.<span class="HOEnZb"><font color="#888888"><br>


<br></font></span></div><span class="HOEnZb"><font color="#888888">Ramana<br></font></span></div>
</blockquote></div><br></div>