[CakeML] Learning material for CakeML

[Magnus Myreen]

Hi Mario,

The tutorial directory is a place where we keep material used for the
tutorials that were held at PLDI'17 and ICFP'17 earlier this year.

You can find examples of verified programs in the following directory.
These programs range from very simple hello-world programs to Unix-style
grep, patch and diff programs.

https://github.com/CakeML/cakeml/tree/master/characteristic/examples

To understand these script files you'll need to know HOL4 quite well and
also understand what the relevant CakeML tools do, e.g. the translator and
the CF framework (and later how to apply the compiler).

For us to help you get started, it might be good to know more about your
aims. Could you tell us what kind of programs you are interested in
verifying? Do you have some example in mind? What is your background?

Cheers,
Magnus


On 17 September 2017 at 22:22, Mario Castelán Castro <marioxcc.MT at yandex.com
> wrote:

> Hello.
>
> I am interested in writing formally verified programs. I have some
> familiarity with the HOL4 system, but not with verifying computer programs.
>
> How I should I learn how to to use CakeML? The only documentation I
> could find is an incomplete manual in the Git repository and a directory
> “tutorial” that is hardly of any help to learn how to use the system.
>
> --
> Do not eat animals; respect them as you respect people.
> https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
>
>
> _______________________________________________
> 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/20170917/a2148235/attachment.html>