[CakeML] Standalones

[Konrad Slind]

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
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.

 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?

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