{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:03:28Z","timestamp":1767927808677,"version":"3.49.0"},"reference-count":58,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T00:00:00Z","timestamp":1686009600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,6,6]]},"abstract":"<jats:p>We present PureCake, a mechanically-verified compiler for PureLang, a lazy, purely functional programming language with monadic effects. PureLang syntax is Haskell-like and indentation-sensitive, and its constraint-based Hindley-Milner type system guarantees safe execution. We derive sound equational reasoning principles over its operational semantics, dramatically simplifying some proofs. We prove end-to-end correctness for the compilation of PureLang down to machine code---the first such result for any lazy language---by targeting CakeML and composing with its verified compiler. Multiple optimisation passes are necessary to handle realistic lazy idioms effectively. We develop PureCake entirely within the HOL4 interactive theorem prover.<\/jats:p>","DOI":"10.1145\/3591259","type":"journal-article","created":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T20:06:24Z","timestamp":1686081984000},"page":"952-976","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["PureCake: A Verified Compiler for a Lazy Functional Language"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3116-0392","authenticated-orcid":false,"given":"Hrutvik","family":"Kanabar","sequence":"first","affiliation":[{"name":"University of Kent, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4224-6132","authenticated-orcid":false,"given":"Samuel","family":"Vivien","sequence":"additional","affiliation":[{"name":"ENS, France \/ Chalmers University of Technology, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4861-2650","authenticated-orcid":false,"given":"Oskar","family":"Abrahamsson","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9504-4107","authenticated-orcid":false,"given":"Magnus O.","family":"Myreen","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1163-8467","authenticated-orcid":false,"given":"Michael","family":"Norrish","sequence":"additional","affiliation":[{"name":"Australian National University, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6406-7875","authenticated-orcid":false,"given":"Johannes \u00c5man","family":"Pohjola","sequence":"additional","affiliation":[{"name":"University of New South Wales, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-3573-6122","authenticated-orcid":false,"given":"Riccardo","family":"Zanetti","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,6,6]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Research Topics in Functional Programming","author":"Abramsky Samson","unstructured":"Samson Abramsky . 1990. The Lazy \u03bb -Calculus . In Research Topics in Functional Programming . Addison Wesley . Samson Abramsky. 1990. The Lazy \u03bb -Calculus. In Research Topics in Functional Programming. Addison Wesley."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429129"},{"key":"e_1_2_1_3_1","volume-title":"Program Logics - for Certified Compilers","author":"Appel Andrew W.","unstructured":"Andrew W. Appel . 2014. Program Logics - for Certified Compilers . Cambridge University Press . isbn:978-1-10-704801-0 http:\/\/www.cambridge.org\/de\/academic\/subjects\/computer-science\/programming-languages-and-applied-logic\/program-logics-certified-compilers?format=HB Andrew W. Appel. 2014. Program Logics - for Certified Compilers. Cambridge University Press. isbn:978-1-10-704801-0 http:\/\/www.cambridge.org\/de\/academic\/subjects\/computer-science\/programming-languages-and-applied-logic\/program-logics-certified-compilers?format=HB"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804312"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236784"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-1(2:1)2005"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41654"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.178047"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706354"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2021.20"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018621"},{"key":"e_1_2_1_12_1","volume-title":"Selective Lambda Lifting. CoRR, abs\/1910.11717","author":"Graf Sebastian","year":"2019","unstructured":"Sebastian Graf and Simon Peyton Jones . 2019. Selective Lambda Lifting. CoRR, abs\/1910.11717 ( 2019 ), arXiv:1910.11717. Sebastian Graf and Simon Peyton Jones. 2019. Selective Lambda Lifting. CoRR, abs\/1910.11717 (2019), arXiv:1910.11717."},{"key":"e_1_2_1_13_1","volume-title":"Operating Systems Design and Implementation (OSDI)","author":"Gu Ronghui","unstructured":"Ronghui Gu , Zhong Shao , Hao Chen , Xiongnan (Newman) Wu , Jieung Kim , Vilhelm Sj\u00f6berg , and David Costanzo . 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels . In Operating Systems Design and Implementation (OSDI) . USENIX Association . https:\/\/doi.org\/10.5555\/3026877.3026928 10.5555\/3026877.3026928 Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In Operating Systems Design and Implementation (OSDI). USENIX Association. https:\/\/doi.org\/10.5555\/3026877.3026928"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341718"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44622-2_21"},{"key":"e_1_2_1_16_1","volume-title":"Top Quality Type Error Messages. Ph. D. Dissertation","author":"Heeren Bastiaan","year":"1874","unstructured":"Bastiaan Heeren . 2005. Top Quality Type Error Messages. Ph. D. Dissertation . Utrecht University , Netherlands. http:\/\/dspace.library.uu.nl\/handle\/ 1874 \/7297 Bastiaan Heeren. 2005. Top Quality Type Error Messages. Ph. D. Dissertation. Utrecht University, Netherlands. http:\/\/dspace.library.uu.nl\/handle\/1874\/7297"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/871895.871902"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.2307\/1995158"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0008"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_35"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/502874.502880"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7782305"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804319"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294106"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158618"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/291891.291892"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373812"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473585"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_16"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19797-5_13"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863584"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292547"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1017\/s095679689900341x"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.1"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439915"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796813000282"},{"key":"e_1_2_1_40_1","volume-title":"Type Inference with Constrained Types. Theory Pract. Object Syst., 5, 1","author":"Odersky Martin","year":"1999","unstructured":"Martin Odersky , Martin Sulzmann , and Martin Wehr . 1999. Type Inference with Constrained Types. Theory Pract. Object Syst., 5, 1 ( 1999 ). Martin Odersky, Martin Sulzmann, and Martin Wehr. 1999. Type Inference with Constrained Types. Theory Pract. Object Syst., 5, 1 (1999)."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_23"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-3236-3_17"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000319"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/3540543961_30"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99385"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2014.10.015"},{"key":"e_1_2_1_47_1","volume-title":"Advanced Topics in Bisimulation and Coinduction","author":"Pitts Andrew M.","unstructured":"Andrew M. Pitts . 2012. Howe\u2019s method for higher-order languages . In Advanced Topics in Bisimulation and Coinduction ( Cambridge tracts in theoretical computer science, Vol. 52). Cambridge University Press. Andrew M. Pitts. 2012. Howe\u2019s method for higher-order languages. In Advanced Topics in Bisimulation and Coinduction (Cambridge tracts in theoretical computer science, Vol. 52). Cambridge University Press."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2022.27"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934564"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-11(1:7)2015"},{"key":"e_1_2_1_51_1","volume-title":"Simon Peyton Jones, and Dimitrios Vytiniotis","author":"Sergey Ilya","year":"2014","unstructured":"Ilya Sergey , Simon Peyton Jones, and Dimitrios Vytiniotis . 2014 . Theory and practice of demand analysis in Haskell. June, https:\/\/core.ac.uk\/display\/357603019 (Unpublished draft) Ilya Sergey, Simon Peyton Jones, and Dimitrios Vytiniotis. 2014. Theory and practice of demand analysis in Haskell. June, https:\/\/core.ac.uk\/display\/357603019 (Unpublished draft)"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591266"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3310232.3310236"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409003"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90147-A"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-18317-5_21"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110275"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591259","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3591259","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:47Z","timestamp":1750178867000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591259"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,6]]},"references-count":58,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2023,6,6]]}},"alternative-id":["10.1145\/3591259"],"URL":"https:\/\/doi.org\/10.1145\/3591259","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,6,6]]},"assertion":[{"value":"2023-06-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}