As far as I know, OpenTheory allows starting to record from a specific point and allows the importer to map constants/types from one prover to similar ones in the other system. -- Magnus<br><div class="gmail_quote"><div dir="ltr">On Thu, 6 Apr 2017 at 12:14, Lars Hupel <<a href="mailto:hupel@in.tum.de">hupel@in.tum.de</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">> What's your timeline for this project, and would you be interested in<br class="gmail_msg">
> working on producing an OpenTheory export of parts of CakeML with my<br class="gmail_msg">
> guidance?<br class="gmail_msg">
<br class="gmail_msg">
The timeline is "eventually" :-)<br class="gmail_msg">
<br class="gmail_msg">
But I'm not sure how well that would work in general. The major problem<br class="gmail_msg">
I foresee is this: You would replay definitions, including datatypes, in<br class="gmail_msg">
Isabelle, right? That means that those datatype definitions would mimic<br class="gmail_msg">
HOL's construction, and not Isabelle's construction. This likely means<br class="gmail_msg">
that I can't do anything useful with them.<br class="gmail_msg">
<br class="gmail_msg">
> Another approach would be to manually port the encoder/decoder definitions,<br class="gmail_msg">
> which might be more expedient but less satisfying and reusable.<br class="gmail_msg">
<br class="gmail_msg">
Not just more expedient but probably also faster. I'll take a stab.<br class="gmail_msg">
<br class="gmail_msg">
> They're not part of the semantics. There's overhead to using Lem, and there<br class="gmail_msg">
> aren't formal guarantees that it produces the same semantics in multiple<br class="gmail_msg">
> systems (although I believe a fair amount of work has gone into ensuring<br class="gmail_msg">
> that is usually the case).<br class="gmail_msg">
<br class="gmail_msg">
Fair enough.<br class="gmail_msg">
<br class="gmail_msg">
Thanks for all the help so far!<br class="gmail_msg">
<br class="gmail_msg">
Cheers<br class="gmail_msg">
Lars<br class="gmail_msg">
<br class="gmail_msg">
_______________________________________________<br class="gmail_msg">
Users mailing list<br class="gmail_msg">
<a href="mailto:Users@cakeml.org" class="gmail_msg" target="_blank">Users@cakeml.org</a><br class="gmail_msg">
<a href="https://lists.cakeml.org/listinfo/users" rel="noreferrer" class="gmail_msg" target="_blank">https://lists.cakeml.org/listinfo/users</a><br class="gmail_msg">
</blockquote></div>