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 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 10:00 | |||
09:00 60mOther | 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 | |||
10:30 1h40mOther | 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 | |||
13:40 1h40mOther | 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 | |||
15:50 70mOther | 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 | ||