<div dir="ltr">To replay the s-expression encode and decode function definitions in Isabelle after recording in OpenTheory, I don't think you would replay any datatype definitions. You already have the CakeML datatypes (from the Lem import), and you can define the sexp datatype manually pretty easily. You would target those existing Isabelle datatypes when importing, as the Magnus and Michael have suggested.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 6 April 2017 at 13:20, <span dir="ltr"><<a href="mailto:Michael.Norrish@data61.csiro.au" target="_blank">Michael.Norrish@data61.csiro.au</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div bgcolor="white" link="blue" vlink="purple" lang="EN-GB">
<div class="m_4426272558726502012WordSection1">
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:Calibri">Absolutely. You can “cut away” the HOL core library’s construction of types and theorems, and record instead the fact that the later CakeML work depends on a
type called ‘a list, with various theorems proved about it. You can then satisfy the requirement to provide such a type and the accompanying theorems with stuff taken from the core Isabelle development.<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:Calibri"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:Calibri">Michael<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:Calibri"><u></u> <u></u></span></p>
<div style="border:none;border-top:solid #b5c4df 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span style="font-family:Calibri;color:black">From: </span>
</b><span style="font-family:Calibri;color:black">Magnus Myreen <<a href="mailto:magnus.myreen@gmail.com" target="_blank">magnus.myreen@gmail.com</a>><br>
<b>Date: </b>Thursday, 6 April 2017 at 21:14<br>
<b>To: </b>Lars Hupel <<a href="mailto:hupel@in.tum.de" target="_blank">hupel@in.tum.de</a>>, Ramana Kumar <<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" target="_blank">Ramana.Kumar@cl.cam.ac.uk</a>><br>
<b>Cc: </b>"<a href="mailto:users@cakeml.org" target="_blank">users@cakeml.org</a>" <<a href="mailto:users@cakeml.org" target="_blank">users@cakeml.org</a>><br>
<b>Subject: </b>Re: [CakeML] Build problems<u></u><u></u></span></p>
</div><div><div class="h5">
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<p class="MsoNormal">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<u></u><u></u></p>
<div>
<div>
<p class="MsoNormal">On Thu, 6 Apr 2017 at 12:14, Lars Hupel <<a href="mailto:hupel@in.tum.de" target="_blank">hupel@in.tum.de</a>> wrote:<u></u><u></u></p>
</div>
<blockquote style="border:none;border-left:solid #cccccc 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm">
<p class="MsoNormal">> What's your timeline for this project, and would you be interested in<br>
> working on producing an OpenTheory export of parts of CakeML with my<br>
> guidance?<br>
<br>
The timeline is "eventually" :-)<br>
<br>
But I'm not sure how well that would work in general. The major problem<br>
I foresee is this: You would replay definitions, including datatypes, in<br>
Isabelle, right? That means that those datatype definitions would mimic<br>
HOL's construction, and not Isabelle's construction. This likely means<br>
that I can't do anything useful with them.<br>
<br>
> Another approach would be to manually port the encoder/decoder definitions,<br>
> which might be more expedient but less satisfying and reusable.<br>
<br>
Not just more expedient but probably also faster. I'll take a stab.<br>
<br>
> They're not part of the semantics. There's overhead to using Lem, and there<br>
> aren't formal guarantees that it produces the same semantics in multiple<br>
> systems (although I believe a fair amount of work has gone into ensuring<br>
> that is usually the case).<br>
<br>
Fair enough.<br>
<br>
Thanks for all the help so far!<br>
<br>
Cheers<br>
Lars<br>
<br>
______________________________<wbr>_________________<br>
Users mailing list<br>
<a href="mailto:Users@cakeml.org" target="_blank">Users@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/users" target="_blank">https://lists.cakeml.org/<wbr>listinfo/users</a><u></u><u></u></p>
</blockquote>
</div>
</div></div></div>
</div>
</blockquote></div><br></div>