{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:48:27Z","timestamp":1775868507162,"version":"3.50.1"},"reference-count":46,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2019,2,4]],"date-time":"2019-02-04T00:00:00Z","timestamp":1549238400000},"content-version":"unspecified","delay-in-days":34,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2019]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The CakeML compiler is, to the best of our knowledge, the most realistic verified compiler for a functional programming language to date. The architecture of the compiler, a sequence of intermediate languages through which high-level features are compiled away incrementally, enables verification of each compilation pass at an appropriate level of semantic detail. Parts of the compiler\u2019s implementation resemble mainstream (unverified) compilers for strict functional languages, and it supports several important features and optimisations. These include efficient curried multi-argument functions, configurable data representations, efficient exceptions, register allocation, and more. The compiler produces machine code for five architectures: x86-64, ARMv6, ARMv8, MIPS-64, and RISC-V. The generated machine code contains the verified runtime system which includes a verified generational copying garbage collector and a verified arbitrary precision arithmetic (bignum) library. In this paper, we present the overall design of the compiler backend, including its 12 intermediate languages. We explain how the semantics and proofs fit together and provide detail on how the compiler has been bootstrapped inside the logic of a theorem prover. The entire development has been carried out within the HOL4 theorem prover.<\/jats:p>","DOI":"10.1017\/s0956796818000229","type":"journal-article","created":{"date-parts":[[2019,2,4]],"date-time":"2019-02-04T09:38:24Z","timestamp":1549273104000},"source":"Crossref","is-referenced-by-count":36,"title":["The verified CakeML compiler backend"],"prefix":"10.1017","volume":"29","author":[{"given":"YONG","family":"KIAM TAN","sequence":"first","affiliation":[]},{"given":"MAGNUS O.","family":"MYREEN","sequence":"additional","affiliation":[]},{"given":"RAMANA","family":"KUMAR","sequence":"additional","affiliation":[]},{"given":"ANTHONY","family":"FOX","sequence":"additional","affiliation":[]},{"given":"SCOTT","family":"OWENS","sequence":"additional","affiliation":[]},{"given":"MICHAEL","family":"NORRISH","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2019,2,4]]},"reference":[{"key":"S0956796818000229_ref37","unstructured":"Romanenko, S. , Russo, C. & Sestoft, P. (2013) Moscow ML owner\u2019s manual, version 2.10. 06."},{"key":"S0956796818000229_ref34","first-page":"18:1","article-title":"Verifying efficient function calls in CakeML","volume":"1","author":"Owens","year":"2017","journal-title":"PACMPL"},{"key":"S0956796818000229_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_23"},{"key":"S0956796818000229_ref31","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784764"},{"key":"S0956796818000229_ref24","unstructured":"MLton Developers (2017). MLton. http:\/\/mlton.org\/."},{"key":"S0956796818000229_ref22","unstructured":"Matthews, D. (2017) Poly\/ML, 5.7 edn. http:\/\/www.polyml.org\/."},{"key":"S0956796818000229_ref19","unstructured":"Kumar, R. 2016 Self-compilation and Self-verification. Technical report, UCAM-CL-TR-879, Computer Laboratory, University of Cambridge."},{"key":"S0956796818000229_ref18","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837642"},{"key":"S0956796818000229_ref17","unstructured":"Hjort, R. , Holmgren, J. & Persson, C. (2017) The CakeML compiler explorer \u2013 Tracking intermediate representations in a verified compiler. In Trends in Functional Programming - 18th International Symposium, (TFP) 2017, Canterbury, UK, June 19\u201321, 2017, Revised Selected Papers, Wang, M. & Owens, S. (eds), Lecture Notes in Computer Science, vol. 10788. Springer, pp. 135\u2013148."},{"key":"S0956796818000229_ref15","unstructured":"Granlund, T. , et al. (2017) GNU MP: The GNU Multiple Precision Arithmetic Library, 6.1.2 edn. http:\/\/gmplib.org\/."},{"key":"S0956796818000229_ref11","unstructured":"Ericsson, A. S. , Myreen, M. O. & Pohjola, J. \u00c5. (2017) A verified generational garbage collector for CakeML. In Interactive Theorem Proving - 8th International Conference, ITP 2017, Bras\u00edlia, Brazil, September 26\u201329, 2017, Proceedings, Ayala-Rinc\u00f3n, M. & Mu\u00f1oz, C. A. (eds). Lecture Notes in Computer Science, vol. 10499. Springer, pp. 444\u2013461."},{"key":"S0956796818000229_ref25","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908109"},{"key":"S0956796818000229_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46663-6_12"},{"key":"S0956796818000229_ref2","unstructured":"Amadio, R. M. , Ayache, N. , Bobot, F. , Boender, J. , Campbell, B. , Garnier, I. , Madet, A. , McKinna, J. , Mulligan, D. P. , Piccolo, M. , Pollack, R. , R\u00e9gis-Gianas, Y. , Coen, C. S. , Stark, I. & Tranquilli, P. (2013) Certified complexity (CerCo). In Foundational and Practical Aspects of Resource Analysis - Third International Workshop, FOPARA 2013, Bertinoro, Italy, August 29\u201331, 2013, Revised Selected Papers, Lago, U. D. & Pe\u00f1a, R. (eds). Lecture Notes in Computer Science, vol. 8552. Springer, pp. 1\u201318."},{"key":"S0956796818000229_ref1","first-page":"118","volume-title":"Trends in Functional Programming - 18th International Symposium, (TFP) 2017","author":"Abrahamsson","year":"2017"},{"key":"S0956796818000229_ref4","volume-title":"Compiling with Continuations","author":"Appel","year":"1992"},{"key":"S0956796818000229_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15057-9_10"},{"key":"S0956796818000229_ref12","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018621"},{"key":"S0956796818000229_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706312"},{"key":"S0956796818000229_ref13","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738006"},{"key":"S0956796818000229_ref29","unstructured":"Myreen, M. O. , Gordon, M. J. C. & Slind, K. (2012) Decompilation into logic \u2013 improved. In Formal Methods in Computer-Aided Design, FMCAD 2012, Cambridge, UK, October 22\u201325, 2012, Cabodi, G. & Singh, S. (eds). IEEE, pp. 78\u201381."},{"key":"S0956796818000229_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_22"},{"key":"S0956796818000229_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11970-5_13"},{"key":"S0956796818000229_ref32","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951940"},{"key":"S0956796818000229_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_9"},{"key":"S0956796818000229_ref36","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9096-8"},{"key":"S0956796818000229_ref7","doi-asserted-by":"publisher","DOI":"10.1145\/2892208.2892211"},{"key":"S0956796818000229_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/2579080"},{"key":"S0956796818000229_ref3","unstructured":"Amadio, R. M. & R\u00e9gis-Gianas, Y. (2011) Certifying and reasoning on cost annotations of functional programs. In Foundational and Practical Aspects of Resource Analysis - Second International Workshop, FOPARA 2011, Madrid, Spain, May 19, 2011, Revised Selected Papers, Pe\u00f1a, R. , van Eekelen, M. C. J. D. & Shkaravska, O. (eds). Lecture Notes in Computer Science, vol. 7177. Springer, pp. 72\u201389."},{"key":"S0956796818000229_ref41","unstructured":"SML\/NJ Developers (2017). SML\/NJ. http:\/\/www.smlnj.org\/."},{"key":"S0956796818000229_ref14","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229546"},{"key":"S0956796818000229_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594301"},{"key":"S0956796818000229_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"S0956796818000229_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"S0956796818000229_ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22863-6_20"},{"key":"S0956796818000229_ref39","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462183"},{"key":"S0956796818000229_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863584"},{"key":"S0956796818000229_ref40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_6"},{"key":"S0956796818000229_ref38","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487248"},{"key":"S0956796818000229_ref42","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676985"},{"key":"S0956796818000229_ref43","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951924"},{"key":"S0956796818000229_ref44","doi-asserted-by":"publisher","DOI":"10.1145\/2897336.2897344"},{"key":"S0956796818000229_ref45","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"S0956796818000229_ref46","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462164"},{"key":"S0956796818000229_ref30","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796813000282"},{"key":"S0956796818000229_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_5"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796818000229","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T23:49:16Z","timestamp":1559951356000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796818000229\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"references-count":46,"alternative-id":["S0956796818000229"],"URL":"https:\/\/doi.org\/10.1017\/s0956796818000229","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"article-number":"e2"}}