Skip to main content

Verifying Efficient Function Calls in CakeML

Owens, Scott, Norrish, Michael, Kumar, Ramana, Myreen, Magnus O., Tan, Yong Kiam (2017) Verifying Efficient Function Calls in CakeML. Proceedings of the ACM Programming Languages, 1 (ICFP). Article Number 18. ISSN 2475-1421. E-ISSN 2475-1421. (doi:10.1145/3110262) (KAR id:62156)

PDF Publisher pdf
Language: English

Download (378kB)
[thumbnail of icfp17.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL:


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.

Item Type: Article
DOI/Identification number: 10.1145/3110262
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Scott Owens
Date Deposited: 27 Jun 2017 16:22 UTC
Last Modified: 10 Dec 2022 13:31 UTC
Resource URI: (The current URI for this page, for reference purposes)
Owens, Scott:
  • Depositors only (login required):


Downloads per month over past year