[CakeML] CakeML Tutorials at PLDI and ICFP

[Ramana Kumar]

Hello everyone,

Just wanted to point out that we are going to run a CakeML tutorial at PLDI
(in 2 weeks!) on Friday June 23rd in Barcelona, as part of the affiliated
PLDI workshops/tutorials. (Sorry for the short notice. There is also one at
ICFP which is months away.)

Here's the info:
http://pldi17.sigplan.org/track/pldi-2017-workshops-and-tutorials
(The CakeML event is the last link on the program)

What's it about? See the following blurb:

Get a taste of program verification in CakeML at PLDI'17!

We are offering a tutorial for students, practitioners, and researchers
alike
on writing and verifying programs in CakeML, the world's foremost verified
ML
implementation. CakeML is a functional programming language and verification
ecosystem backed by the higher-order logic (HOL) theorem prover. We will
show
you how to write useful programs in CakeML, prove their correctness, and
leverage the verified optimising CakeML compiler to obtain a trustworthy and
efficient executable.

In this tutorial, you will get hands-on experience with
  - writing programs in CakeML,
  - proving program specifications in HOL,
  - producing verified CakeML automatically from verified algorithms in
HOL, and
  - interactively verifying imperative CakeML programs that do I/O.

Participants are expected to have some prior exposure to functional
programming, however no experience with interactive theorem proving or
verification is required. At the same time, there is plenty of scope for
verification experts to dive in and learn something new.

We will also run a half-day version of this tutorial at ICFP (in September)
in Oxford.

Looking forward to possibly seeing some of you at one of these events!

Cheers,
Ramana
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20170606/71f9d0f4/attachment.html>