Skip to main content
Home

Main navigation

  • Home
  • Series
  • People
  • Depts & Colleges
  • Open Education

Main navigation

  • Home
  • Series
  • People
  • Depts & Colleges
  • Open Education

Verifying Efficient Function Calls in CakeML

Series
International Conference on Functional Programming 2017
Video Embed
Scott Owens University of Kent, UK, gives the third talk in the first panel, Low-level and Systems Programming, on the 2nd day of the ICFP conference.
Co-written Michael Norrish, Ramana Kumar (Data61 at CSIRO, Australia and UNSW, Australia), Magnus O. Myreen (Chalmers University of Technology, Sweden), Yong Kiam Tan (Carnegie Mellon University, USA).

We have designed an intermediate language (IL) for the CakeML compiler that supports the verified, efficient compilation of functions and calls. Verified compilation steps include batching of multiple curried arguments, detecting calls to statically known functions, and specialising calls to known functions with no free variables. Finally, we verify the translation to a lower-level IL that only supports closed, first-order functions.

These compilation steps resemble those found in other compilers (especially OCaml). Our contribution here is the design of the semantics of the IL, and the demonstration that our verification techniques over this semantics work well in practice at this scale. The entire development was carried out in the HOL4 theorem prover.

More in this series

View Series
International Conference on Functional Programming 2017

A Relational Logic for Higher-Order Programs

Alejandro Aguirre, IMDEA Software Institute, Spain, gives the second talk in the second panel, Foundations of Higher-Order Programming, on the 2nd day of the ICFP conference.
Previous
International Conference on Functional Programming 2017

Better Living through Operational Semantics: An Optimizing Compiler for Radio Protocols

Geoffrey Mainland (Drexel University, USA) gives the fourth talk in the first panel, Low-level and Systems Programming, on the 2nd day of the ICFP conference.
Next
Licence
Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK: England & Wales; http://creativecommons.org/licenses/by-nc-sa/2.0/uk/

Episode Information

Series
International Conference on Functional Programming 2017
People
Scott Owens
Keywords
technology
computing
programming
Department: Department of Computer Science
Date Added: 18/12/2017
Duration: 00:19:53

Subscribe

Apple Podcast Video Video RSS Feed

Download

Download Video

Footer

  • About
  • Accessibility
  • Contribute
  • Copyright
  • Contact
  • Privacy
'Oxford Podcasts' Twitter Account @oxfordpodcasts | MediaPub Publishing Portal for Oxford Podcast Contributors | Upcoming Talks in Oxford | © 2011-2022 The University of Oxford