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.
Tue 5 SepDisplayed time zone: Belfast change
10:30 - 12:00
|Persistence for the Masses: RRB-Vectors in a Systems Language|
Juan Pedro Bolívar Puente Independent Consultant, Sinusoidal EngineeringDOI Pre-print
|Verified Low-Level Programming Embedded in F*|
Jonathan Protzenko Microsoft Research, n.n., Jean-Karim Zinzindohoué Inria, France, Aseem Rastogi Microsoft Research, Tahina Ramananandro Microsoft Research, n.n., Peng Wang Massachusetts Institute of Technology, USA, Santiago Zanella-Béguelin Microsoft Research, n.n., Antoine Delignat-Lavaud Microsoft Research, n.n., Cătălin Hriţcu Inria Paris, Karthikeyan Bhargavan Inria, France, Cédric Fournet Microsoft Research, n.n., Nikhil Swamy Microsoft Research, n.n.DOI
|Verifying Efficient Function Calls in CakeML|
Scott Owens University of Kent, UK, Michael Norrish Data61 at CSIRO, Australia / Australian National University, Australia, Ramana Kumar Data61 at CSIRO, Australia / UNSW, Australia, Magnus O. Myreen Chalmers University of Technology, Sweden, Yong Kiam Tan Carnegie Mellon University, USADOI
|Better Living through Operational Semantics: An Optimizing Compiler for Radio Protocols|
Geoffrey Mainland Drexel University, USADOI