{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T00:48:32Z","timestamp":1772498912690,"version":"3.50.1"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2019,7,26]],"date-time":"2019-07-26T00:00:00Z","timestamp":1564099200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1816837, CCF-1618732, CCF-1453796, CCF-1422133"],"award-info":[{"award-number":["CCF-1816837, CCF-1618732, CCF-1453796, CCF-1422133"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,7,26]]},"abstract":"<jats:p>Compiler correctness is an old problem, with results stretching back beyond the last half-century. Founding the field, John McCarthy and James Painter set out to build a \"completely trustworthy compiler\". And yet, until quite recently, even despite truly impressive verification efforts, the theorems being proved were only about the compilation of whole programs, a theoretically quite appealing but practically unrealistic simplification. For a compiler correctness theorem to assure complete trust, the theorem must reflect the reality of how the compiler will be used.<\/jats:p>\n          <jats:p>There has been much recent work on more realistic \"compositional\" compiler correctness aimed at proving correct compilation of components while supporting linking with components compiled from different languages using different compilers. However, the variety of theorems, stated in remarkably different ways, raises questions about what researchers even mean by a \"compiler is correct.\" In this pearl, we develop a new framework with which to understand compiler correctness theorems in the presence of linking, and apply it to understanding and comparing this diversity of results. In doing so, not only are we better able to assess their relative strengths and weaknesses, but gain insight into what we as a community should expect from compiler correctness theorems of the future.<\/jats:p>","DOI":"10.1145\/3341689","type":"journal-article","created":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T20:55:51Z","timestamp":1564433751000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":24,"title":["The next 700 compiler correctness theorems (functional pearl)"],"prefix":"10.1145","volume":"3","author":[{"given":"Daniel","family":"Patterson","sequence":"first","affiliation":[{"name":"Northeastern University, USA"}]},{"given":"Amal","family":"Ahmed","sequence":"additional","affiliation":[{"name":"Northeastern University, USA"}]}],"member":"320","published-online":{"date-parts":[[2019,7,26]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"key":"e_1_2_2_2_1","volume-title":"1st Summit on Advances in Programming Languages (SNAPL 2015) (Leibniz International Proceedings in Informatics (LIPIcs)), Thomas Ball, Rastislav Bodik, Shriram Krishnamurthi, Benjamin S","author":"Ahmed Amal","unstructured":"Amal Ahmed . 2015. Verified Compilers for a Multi-Language World . In 1st Summit on Advances in Programming Languages (SNAPL 2015) (Leibniz International Proceedings in Informatics (LIPIcs)), Thomas Ball, Rastislav Bodik, Shriram Krishnamurthi, Benjamin S . Lerner, and Greg Morrisett (Eds.), Vol. 32 . 15\u201331. Amal Ahmed. 2015. Verified Compilers for a Multi-Language World. In 1st Summit on Advances in Programming Languages (SNAPL 2015) (Leibniz International Proceedings in Informatics (LIPIcs)), Thomas Ball, Rastislav Bodik, Shriram Krishnamurthi, Benjamin S. Lerner, and Greg Morrisett (Eds.), Vol. 32. 15\u201331."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411227"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034830"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480925"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596567"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_7"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784733"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250742"},{"key":"e_1_2_2_10_1","volume-title":"Science of Computer Programming","author":"Felleisen Matthias","unstructured":"Matthias Felleisen . 1990. On the Expressive Power of Programming Languages . In Science of Computer Programming . Springer-Verlag , 134\u2013151. Matthias Felleisen. 1990. On the Expressive Power of Programming Languages. In Science of Computer Programming. Springer-Verlag, 134\u2013151."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926402"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314595"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837642"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_2_2_17_1","volume-title":"Under Control: Compositionally Correct Closure Conversion with Mutable State. In ACM Conference on Principles and Practice of Declarative Programming (PPDP).","author":"Mates Phillip","year":"2019","unstructured":"Phillip Mates , Jamie Perconti , and Amal Ahmed . 2019 . Under Control: Compositionally Correct Closure Conversion with Mutable State. In ACM Conference on Principles and Practice of Declarative Programming (PPDP). Phillip Mates, Jamie Perconti, and Amal Ahmed. 2019. Under Control: Compositionally Correct Closure Conversion with Mutable State. In ACM Conference on Principles and Practice of Declarative Programming (PPDP)."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190220"},{"key":"e_1_2_2_19_1","doi-asserted-by":"crossref","unstructured":"John McCarthy. 1959. A Basis for a Mathematical Theory of Computation. Studies in Logic and the Foundations of Mathematics 33\u201370.   John McCarthy. 1959. A Basis for a Mathematical Theory of Computation. Studies in Logic and the Foundations of Mathematics 33\u201370.","DOI":"10.1016\/S0049-237X(09)70099-0"},{"key":"e_1_2_2_20_1","volume-title":"Correctness of a compiler for arithmetic expressions","author":"McCarthy John","unstructured":"John McCarthy and James Painter . 1967. Correctness of a compiler for arithmetic expressions . American Mathematical Society , 33\u201341. John McCarthy and James Painter. 1967. Correctness of a compiler for arithmetic expressions. American Mathematical Society, 33\u201341."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237791"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/512927.512941"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784764"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951941"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951940"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699503"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3280984"},{"key":"e_1_2_2_28_1","volume-title":"2nd Summit on Advances in Programming Languages (SNAPL 2017) (Leibniz International Proceedings in Informatics (LIPIcs)), Benjamin S","author":"Patterson Daniel","unstructured":"Daniel Patterson and Amal Ahmed . 2017. Linking Types for Multi-Language Software: Have Your Cake and Eat It Too . In 2nd Summit on Advances in Programming Languages (SNAPL 2017) (Leibniz International Proceedings in Informatics (LIPIcs)), Benjamin S . Lerner, Rastislav Bod\u00edk, and Shriram Krishnamurthi (Eds.), Vol. 71 . Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany , 12:1\u201312:15. Daniel Patterson and Amal Ahmed. 2017. Linking Types for Multi-Language Software: Have Your Cake and Eat It Too. In 2nd Summit on Advances in Programming Languages (SNAPL 2017) (Leibniz International Proceedings in Informatics (LIPIcs)), Benjamin S. Lerner, Rastislav Bod\u00edk, and Shriram Krishnamurthi (Eds.), Vol. 71. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 12:1\u201312:15."},{"key":"e_1_2_2_29_1","volume-title":"CCC: Supplementary Materials. https:\/\/dbp.io\/pubs\/2019\/ccc\/","author":"Patterson Daniel","year":"2019","unstructured":"Daniel Patterson and Amal Ahmed . 2019 . CCC: Supplementary Materials. https:\/\/dbp.io\/pubs\/2019\/ccc\/ Daniel Patterson and Amal Ahmed. 2019. CCC: Supplementary Materials. https:\/\/dbp.io\/pubs\/2019\/ccc\/"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062347"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_8"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676724.2693167"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/PROC.1975.9939"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926393"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676985"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660201"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290375"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341689","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341689","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341689","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:30Z","timestamp":1750200090000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341689"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,26]]},"references-count":38,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2019,7,26]]}},"alternative-id":["10.1145\/3341689"],"URL":"https:\/\/doi.org\/10.1145\/3341689","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,7,26]]},"assertion":[{"value":"2019-07-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}