[CakeML] Standalones

Konrad Slind konrad.slind at gmail.com
Mon Jan 27 18:45:40 UTC 2014

Hi all,

  First, congratulations Ramana for the excellent talk at POPL. I thought it
was very well received.

 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
were small enough, I could just run the compiler inside the logic, obtain
bytecodes, run the bytecode compiler (if that's what it is) and get the
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.
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.

 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?

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20140127/2a06842b/attachment.html>

More information about the Users mailing list