{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T00:48:31Z","timestamp":1772498911096,"version":"3.50.1"},"reference-count":64,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T00:00:00Z","timestamp":1629331200000},"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-1521602 and CCF-2005545"],"award-info":[{"award-number":["CCF-1521602 and CCF-2005545"]}],"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":[[2021,8,22]]},"abstract":"<jats:p>\n            Compositional compiler verification is a difficult problem that focuses on separate compilation of program components with possibly different verified compilers. Logical relations are widely used in proving correctness of program transformations in higher-order languages; however, they do not scale to compositional verification of multi-pass compilers due to their lack of transitivity. The only known technique to apply to compositional verification of multi-pass compilers for higher-order languages is parametric inter-language simulations (PILS), which is however significantly more complicated than traditional proof techniques for compiler correctness. In this paper, we present a novel verification framework for\n            <jats:italic>lightweight compositional compiler correctness<\/jats:italic>\n            . We demonstrate that by imposing the additional restriction that program components are compiled by pipelines that go through\n            <jats:italic>the same sequence of intermediate representations<\/jats:italic>\n            , logical relation proofs can be transitively composed in order to derive an end-to-end compositional specification for multi-pass compiler pipelines. Unlike traditional logical-relation frameworks, our framework supports divergence preservation\u2014even when transformations reduce the number of program steps. We achieve this by parameterizing our logical relations with a pair of\n            <jats:italic>relational invariants<\/jats:italic>\n            .\n          <\/jats:p>\n          <jats:p>We apply this technique to verify a multi-pass, optimizing middle-end pipeline for CertiCoq, a compiler from Gallina (Coq\u2019s specification language) to C. The pipeline optimizes and closure-converts an untyped functional intermediate language (ANF or CPS) to a subset of that language without nested functions, which can be easily code-generated to low-level languages. Notably, our pipeline performs more complex closure-allocation optimizations than the state of the art in verified compilation. Using our novel verification framework, we prove an end-to-end theorem for our pipeline that covers both termination and divergence and applies to whole-program and separate compilation, even when different modules are compiled with different optimizations. Our results are mechanized in the Coq proof assistant.<\/jats:p>","DOI":"10.1145\/3473591","type":"journal-article","created":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T10:44:29Z","timestamp":1629369869000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Compositional optimizations for CertiCoq"],"prefix":"10.1145","volume":"5","author":[{"given":"Zoe","family":"Paraskevopoulou","sequence":"first","affiliation":[{"name":"Northeastern University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John M.","family":"Li","sequence":"additional","affiliation":[{"name":"Princeton University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew W.","family":"Appel","sequence":"additional","affiliation":[{"name":"Princeton University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,8,19]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328476"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/12276.13333"},{"key":"e_1_2_2_3_1","doi-asserted-by":"crossref","volume-title":"Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types","author":"Ahmed Amal","DOI":"10.1007\/11693024_6"},{"key":"e_1_2_2_4_1","volume-title":"CoqPL\u201917: The Third International Workshop on Coq for Programming Languages. 2 pages.","author":"Anand Abhishek","year":"2017"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002839"},{"key":"e_1_2_2_6_1","volume-title":"Compiling with Continuations","author":"Appel Andrew W."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2701415"},{"key":"e_1_2_2_8_1","unstructured":"Andrew W. Appel. 2020. Verified Functional Algorithms. Version 1.4 http:\/\/softwarefoundations.cis.upenn.edu  Andrew W. Appel. 2020. Verified Functional Algorithms. Version 1.4 http:\/\/softwarefoundations.cis.upenn.edu"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002839"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371075"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596567"},{"key":"e_1_2_2_13_1","volume-title":"Implementation and Application of Functional Languages, Clemens Grelck, Frank Huch, Greg J","author":"Benton Nick","year":"2038"},{"key":"e_1_2_2_14_1","volume-title":"Register allocation via coloring. Computer languages, 6, 1","author":"Chaitin Gregory J","year":"1981"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706312"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1779419.1779436"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155113"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/114005.102805"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434287"},{"key":"e_1_2_2_20_1","volume-title":"Selective Lambda Lifting. CoRR, abs\/1910.11717","author":"Graf Sebastian","year":"2019"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_2_2_22_1","volume-title":"Super-Combinators: A New Implementation Method for Applicative Languages. In In Conference Record of the 1982 ACM Symposium on Lisp and Functional Programming. ACM, 1\u201310","author":"Hughes R. J. M.","year":"1982"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926402"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103666"},{"key":"e_1_2_2_25_1","volume-title":"Parametric Bisimulations: A Logical Step Forward.","author":"Hur Neis Georg","year":"2014"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/5280.5292"},{"key":"e_1_2_2_27_1","volume-title":"Programming Languages and Systems \u2014 ESOP \u201996","author":"Peyton Jones Simon L."},{"key":"e_1_2_2_28_1","volume-title":"Functional Programming, Glasgow","author":"Jones Simon Peyton","year":"1994"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837642"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75302"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291179"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535841"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_2_2_35_1","unstructured":"Xavier Leroy Damien Doligez Alain Frisch Jacques Garrigue Didier R\u00e9my and J\u00e9r\u00f4me Vouillon. 2020. The OCaml system release 4.11. Available electronically at https:\/\/coq.inria.fr\/refman  Xavier Leroy Damien Doligez Alain Frisch Jacques Garrigue Didier R\u00e9my and J\u00e9r\u00f4me Vouillon. 2020. The OCaml system release 4.11. Available electronically at https:\/\/coq.inria.fr\/refman"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.12.004"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190220"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062380"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167089"},{"key":"e_1_2_2_40_1","doi-asserted-by":"crossref","unstructured":"Juan Antonio Navarro P\u00e9rez and Andrey Rybalchenko. 2011. Separation logic + superposition calculus = heap theorem prover. In PLDI. 556\u2013566.  Juan Antonio Navarro P\u00e9rez and Andrey Rybalchenko. 2011. Separation logic + superposition calculus = heap theorem prover. In PLDI. 556\u2013566.","DOI":"10.1145\/1993316.1993563"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784764"},{"key":"e_1_2_2_42_1","volume-title":"Functional Big-Step Semantics","author":"Owens Scott"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110262"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341687"},{"key":"e_1_2_2_45_1","doi-asserted-by":"crossref","unstructured":"Zoe Paraskevopoulou and Anvay Grover. 2021. Compiling with Continuations Correctly. Under submission.  Zoe Paraskevopoulou and Anvay Grover. 2021. Compiling with Continuations Correctly. Under submission.","DOI":"10.1145\/3485491"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341689"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_8"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676724.2693167"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2016.06.013"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3131851.3131859"},{"key":"e_1_2_2_53_1","volume-title":"Appel","author":"B\u00e9langer Olivier Savary","year":"2019"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/182409.156783"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345125"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371091"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371076"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.5555\/889478"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364531"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676985"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951924"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000229"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158152"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/359460.359478"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290375"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3473591","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3473591","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3473591","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:28:16Z","timestamp":1750195696000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3473591"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,19]]},"references-count":64,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2021,8,22]]}},"alternative-id":["10.1145\/3473591"],"URL":"https:\/\/doi.org\/10.1145\/3473591","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,8,19]]},"assertion":[{"value":"2021-08-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}