Blogs (28) >>
ICFP 2017
Sun 3 - Sat 9 September 2017 Oxford, United Kingdom
Tue 5 Sep 2017 11:15 - 11:37 at L1 - Low-level and Systems Programming Chair(s): Sam Tobin-Hochstadt

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 Sep

10:30 - 12:00: Research Papers - Low-level and Systems Programming at L1
Chair(s): Sam Tobin-HochstadtIndiana University
icfp-2017-papers150460020000010:30 - 10:52
Juan Pedro Bolívar PuenteIndependent Consultant, Sinusoidal Engineering
DOI Pre-print
icfp-2017-papers150460155000010:52 - 11:15
Jonathan ProtzenkoMicrosoft Research, n.n., Jean-Karim ZinzindohouéInria, France, Aseem RastogiMicrosoft Research, Tahina RamananandroMicrosoft Research, n.n., Peng WangMassachusetts Institute of Technology, USA, Santiago Zanella-BéguelinMicrosoft Research, n.n., Antoine Delignat-LavaudMicrosoft Research, n.n., Cătălin HriţcuInria Paris, Karthikeyan BhargavanInria, France, Cédric FournetMicrosoft Research, n.n., Nikhil SwamyMicrosoft Research, n.n.
icfp-2017-papers150460290000011:15 - 11:37
Scott OwensUniversity of Kent, UK, Michael NorrishData61 at CSIRO, Australia / Australian National University, Australia, Ramana KumarData61 at CSIRO, Australia / UNSW, Australia, Magnus O. MyreenChalmers University of Technology, Sweden, Yong Kiam TanCarnegie Mellon University, USA
icfp-2017-papers150460425000011:37 - 12:00
Geoffrey MainlandDrexel University, USA