[CakeML] Standalones

Konrad Slind konrad.slind at gmail.com
Thu Jan 30 17:28:50 UTC 2014


Good luck with the writing. Like Freek, I'd be happy to comment on drafts.

Konrad.



On Tue, Jan 28, 2014 at 6:02 AM, Magnus Myreen
<magnus.myreen at cl.cam.ac.uk>wrote:

> On 28 January 2014 08:18, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
> > On Mon, Jan 27, 2014 at 10:45 AM, Konrad Slind <konrad.slind at gmail.com>
> wrote:
> >>   First, congratulations Ramana for the excellent talk at POPL. I
> thought it
> >> was very well received.
> >
> > Thank you!
> >
> >>  Scott and I talked about how to get standalone executables that I can
> prove
> >> properties about at the HOL function level. He reckoned that if the
> >> functions
> >> were small enough, I could just run the compiler inside the logic,
> obtain
> >> the
> >> bytecodes, run the bytecode compiler (if that's what it is) and get the
> x86.
> >> I would then need to write my own small C wrapper that initalized the
> cakeML
> >> runtime system such that the relevant properties it needs are satisfied.
> >> Then
> >> jump to the compiled code and run.
> >>
> >>   If that's not a bad idea (seemed plausible to me) I will get started
> on
> >> that for
> >> some small programs to see whether it is possible.
> >
> > Indeed that does sound like a good idea. The first step is getting a
> > CakeML version of your program, which is the job of the translator.
> > You can see how this is done for QSORT in
> > translator/ml_translator_demoScript.sml. Once you have the certified
> > CakeML program, then you can either run the compiler on it in the
> > logic or run it in the (as-yet-non-existent) compiler outside the
> > logic. I'll be happy to work with you on making that work (both ways
> > eventually, but at least the first way) after submitting to ITP.
> >
> >>
> >>  I will still need to get the system built. I would also like to get the
> >> REPL built
> >> so that I can play with it. What is the status of that?
> >
> > I'll let Magnus answer, since he has been working on it most recently.
>
> I'm also in a hurry to get ready for the ITP deadline. The status of
> the machine-code implementation is that it's incomplete, due to a few
> remaining cheats in the proof and a few bugs I've found in the
> underlying x86 model. I'll update you as soon as there's news
> regarding the implementation.
>
> Cheers,
> Magnus
>
> >>
> >> Thanks,
> >> Konrad.
> >>
> >>
> >>
> >> _______________________________________________
> >> Users mailing list
> >> Users at cakeml.org
> >> https://lists.cakeml.org/listinfo/users
> >>
> >
> > _______________________________________________
> > Users mailing list
> > Users at cakeml.org
> > https://lists.cakeml.org/listinfo/users
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20140130/c425d96b/attachment.html>


More information about the Users mailing list