konrad.slind at gmail.com
Mon Jan 27 18:45:40 UTC 2014
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
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
so that I can play with it. What is the status of that?
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Users