[CakeML] CakeML User Guide / Tutorial

Ramana Kumar Ramana.Kumar at cl.cam.ac.uk
Sun May 1 06:14:39 UTC 2016


Hi Yves,

Currently, as far as I am aware, there is no documentation or tutorials on
how to program with CakeML.
However, I hope there will be some day soon. More concretely, I have plans
to help write a book on using CakeML early next year.

In the meantime, playing around and asking questions on the mailing list is
very welcome.
Currently, I think the only way to run version 2 of the compiler is by
rewriting its definition in the logic, following the script in
compiler/eval/example/example.sml.
To run version 1, however, you can simply download it from the CakeML
website and follow the simple instructions there.
We hope to produce an executable REPL of version 2 of the compiler within a
month or two.

Programming in CakeML can be very much like programming in Standard ML.
However, to produce verified programs with CakeML (which is its intended
strength) there are two main approaches, and the first is slightly
different from normal unverified programming. The approaches are: 1. Write
your program as a function in HOL, verify it as usual, and use the
HOL-to-CakeML translator to produce the verified implementation in CakeML;
or 2. Write your program in CakeML directly, then use the CakeML-to-HOL
translator (which currently does not exist) to produce characteristic
formulae over which you can verify your program in HOL.

I'm very sorry I cannot point you to documentation yet, but I hope I will
be able to later.

Ramana

On 1 May 2016 at 10:42, Yves Cloutier <yves.cloutier at gmail.com> wrote:

> Hello,
>
> I would like to know if there is ducomentation or tutorials on how to
> program with CakeML?
>
> Regards,
>
> yves
>
> _______________________________________________
> 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/20160501/dce7d7eb/attachment.html>


More information about the Users mailing list