Show simple item record

dc.contributor.authorTan, YKen
dc.contributor.authorMyreen, MOen
dc.contributor.authorKumar, Ren
dc.contributor.authorFox, Anthonyen
dc.contributor.authorOwens, Sen
dc.contributor.authorNorrish, Men
dc.date.accessioned2016-11-30T13:31:38Z
dc.date.available2016-11-30T13:31:38Z
dc.date.issued2016-09-04en
dc.identifier.issn1523-2867
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/261357
dc.description.abstractWe have developed and mechanically verified a new compiler backend for CakeML. Our new compiler features a sequence of intermediate languages that allows it to incrementally compile away high-level features and enables verification at the right levels of semantic detail. In this way, it resembles mainstream (unverified) compilers for strict functional languages. The compiler supports efficient curried multi-argument functions, configurable data representations, exceptions that unwind the call stack, register allocation, and more. The compiler targets several architectures: x86-64, ARMv6, ARMv8, MIPS-64, and RISC-V. In this paper, we present the overall structure of the compiler, including its 12 intermediate languages, and explain how everything fits together. We focus particularly on the interaction between the verification of the register allocator and the garbage collector, and memory representations. The entire development has been carried out within the HOL4 theorem prover.
dc.description.sponsorshipEngineering and Physical Sciences Research Council
dc.language.isoenen
dc.publisherAssociation for Computing Machinery
dc.subjectcompiler verificationen
dc.subjectMLen
dc.subjectverified optimisationsen
dc.titleA New Verified Compiler Backend for CakeMLen
dc.typeArticle
prism.endingPage73
prism.publicationDate2016en
prism.publicationNameProceedings of the 21st ACM SIGPLAN International Conference on Functional Programmingen
prism.startingPage60
dc.identifier.doi10.17863/CAM.6525
dcterms.dateAccepted2016-07-05en
rioxxterms.versionofrecord10.1145/2951913.2951924en
rioxxterms.versionAMen
rioxxterms.licenseref.urihttp://www.rioxx.net/licenses/all-rights-reserveden
rioxxterms.licenseref.startdate2016-09-04en
dc.contributor.orcidFox, Anthony [0000-0002-1564-3784]
dc.identifier.eissn1558-1160
rioxxterms.typeJournal Article/Reviewen
pubs.funder-project-idEPSRC (EP/K008528/1)


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record