Write a Blog >>
Fri 23 Jun 2017 09:00 - 10:00 at Vertex WS219 - Writing Verified Programs in CakeML
Fri 23 Jun 2017 10:30 - 12:10 at Vertex WS219 - Writing Verified Programs in CakeML (2)
Fri 23 Jun 2017 13:40 - 15:20 at Vertex WS219 - Writing Verified Programs in CakeML (3)
Fri 23 Jun 2017 15:50 - 17:00 at Vertex WS219 - Writing Verified Programs in CakeML (4)

Get a taste of program verification in CakeML!

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.

Fri 23 Jun
Times are displayed in time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

pldi-2017-workshops-and-tutorials
09:00 - 10:00: PLDI Tutorials - Writing Verified Programs in CakeML at Vertex WS219
pldi-2017-workshops-and-tutorials09:00 - 10:00
Other
Ramana KumarData61 at CSIRO, Australia / UNSW, Australia, Michael NorrishData61 at CSIRO, Australia / Australian National University, Australia, Scott OwensUniversity of Kent, UK, Magnus O. MyreenChalmers University of Technology, Sweden
Link to publication
pldi-2017-workshops-and-tutorials
10:30 - 12:10: PLDI Tutorials - Writing Verified Programs in CakeML (2) at Vertex WS219
pldi-2017-workshops-and-tutorials10:30 - 12:10
Other
Ramana KumarData61 at CSIRO, Australia / UNSW, Australia, Michael NorrishData61 at CSIRO, Australia / Australian National University, Australia, Scott OwensUniversity of Kent, UK, Magnus O. MyreenChalmers University of Technology, Sweden
Link to publication
pldi-2017-workshops-and-tutorials
13:40 - 15:20: PLDI Tutorials - Writing Verified Programs in CakeML (3) at Vertex WS219
pldi-2017-workshops-and-tutorials13:40 - 15:20
Other
Ramana KumarData61 at CSIRO, Australia / UNSW, Australia, Michael NorrishData61 at CSIRO, Australia / Australian National University, Australia, Scott OwensUniversity of Kent, UK, Magnus O. MyreenChalmers University of Technology, Sweden
Link to publication
pldi-2017-workshops-and-tutorials
15:50 - 17:00: PLDI Tutorials - Writing Verified Programs in CakeML (4) at Vertex WS219
pldi-2017-workshops-and-tutorials15:50 - 17:00
Other
Ramana KumarData61 at CSIRO, Australia / UNSW, Australia, Michael NorrishData61 at CSIRO, Australia / Australian National University, Australia, Scott OwensUniversity of Kent, UK, Magnus O. MyreenChalmers University of Technology, Sweden
Link to publication