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

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00
Writing Verified Programs in CakeMLPLDI Tutorials at Vertex WS219
09:00
60m
Other
Writing Verified Programs in CakeML
PLDI Tutorials
Ramana Kumar Data61 at CSIRO, Australia / UNSW, Australia, Michael Norrish Data61 at CSIRO, Australia / Australian National University, Australia, Scott Owens University of Kent, UK, Magnus O. Myreen Chalmers University of Technology, Sweden
Link to publication
10:30 - 12:10
Writing Verified Programs in CakeML (2)PLDI Tutorials at Vertex WS219
10:30
1h40m
Other
Writing Verified Programs in CakeML
PLDI Tutorials
Ramana Kumar Data61 at CSIRO, Australia / UNSW, Australia, Michael Norrish Data61 at CSIRO, Australia / Australian National University, Australia, Scott Owens University of Kent, UK, Magnus O. Myreen Chalmers University of Technology, Sweden
Link to publication
13:40 - 15:20
Writing Verified Programs in CakeML (3)PLDI Tutorials at Vertex WS219
13:40
1h40m
Other
Writing Verified Programs in CakeML
PLDI Tutorials
Ramana Kumar Data61 at CSIRO, Australia / UNSW, Australia, Michael Norrish Data61 at CSIRO, Australia / Australian National University, Australia, Scott Owens University of Kent, UK, Magnus O. Myreen Chalmers University of Technology, Sweden
Link to publication
15:50 - 17:00
Writing Verified Programs in CakeML (4)PLDI Tutorials at Vertex WS219
15:50
70m
Other
Writing Verified Programs in CakeML
PLDI Tutorials
Ramana Kumar Data61 at CSIRO, Australia / UNSW, Australia, Michael Norrish Data61 at CSIRO, Australia / Australian National University, Australia, Scott Owens University of Kent, UK, Magnus O. Myreen Chalmers University of Technology, Sweden
Link to publication