{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,5]],"date-time":"2026-05-05T07:02:24Z","timestamp":1777964544993,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":58,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,6,9]],"date-time":"2022-06-09T00:00:00Z","timestamp":1654732800000},"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":[],"published-print":{"date-parts":[[2022,6,9]]},"DOI":"10.1145\/3519939.3523706","type":"proceedings-article","created":{"date-parts":[[2022,6,2]],"date-time":"2022-06-02T21:05:05Z","timestamp":1654203905000},"page":"918-933","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code"],"prefix":"10.1145","author":[{"given":"Cl\u00e9ment","family":"Pit-Claudel","sequence":"first","affiliation":[{"name":"EPFL, Switzerland \/ Amazon AWS, Switzerland"}]},{"given":"Jade","family":"Philipoom","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"given":"Dustin","family":"Jamner","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"given":"Andres","family":"Erbsen","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"given":"Adam","family":"Chlipala","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]}],"member":"320","published-online":{"date-parts":[[2022,6,9]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"CertiCoq: A Verified Compiler for Coq. In 3rd International Workshop on Coq for PL (CoqPL","author":"Anand Abhishek","year":"2017","unstructured":"Abhishek Anand , Andrew Appel , Greg Morrisett , Zoe Paraskevopoulou , Randy Pollack , Olivier Savary Belanger , Matthieu Sozeau , and Matthew Weaver . 2017 . CertiCoq: A Verified Compiler for Coq. In 3rd International Workshop on Coq for PL (CoqPL 2017). Abhishek Anand, Andrew Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Belanger, Matthieu Sozeau, and Matthew Weaver. 2017. CertiCoq: A Verified Compiler for Coq. In 3rd International Workshop on Coq for PL (CoqPL 2017)."},{"key":"e_1_3_2_1_2_1","volume-title":"Verified Software Toolchain. In 20th European Conference on Programming Languages and Systems (ESOP 2011","author":"Appel Andrew W.","year":"2011","unstructured":"Andrew W. Appel . 2011 . Verified Software Toolchain. In 20th European Conference on Programming Languages and Systems (ESOP 2011 ). Springer-Verlag, Berlin, Heidelberg. 1\u201317. isbn:9783642 197178 Andrew W. Appel. 2011. Verified Software Toolchain. In 20th European Conference on Programming Languages and Systems (ESOP 2011). Springer-Verlag, Berlin, Heidelberg. 1\u201317. isbn:9783642197178"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_3_2_1_4_1","unstructured":"Pierre Chambart Mark Shinwell Damien Doligez and OCaml Contributors. 2016. Optimization with FLambda. https:\/\/ocaml.org\/manual\/flambda.html  Pierre Chambart Mark Shinwell Damien Doligez and OCaml Contributors. 2016. Optimization with FLambda. https:\/\/ocaml.org\/manual\/flambda.html"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677006"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57840-4_34"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454065"},{"key":"e_1_3_2_1_9_1","volume-title":"10th International Conference on Interactive Theorem Proving (ITP","author":"Forster Yannick","year":"2019","unstructured":"Yannick Forster and Fabian Kunze . 2019 . A certifying extraction with time bounds from Coq to call-by-value \u03bb-calculus . In 10th International Conference on Interactive Theorem Proving (ITP 2019). Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik, 17:1\u201317:19. Yannick Forster and Fabian Kunze. 2019. A certifying extraction with time bounds from Coq to call-by-value \u03bb-calculus. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik, 17:1\u201317:19."},{"key":"e_1_3_2_1_10_1","unstructured":"Konstantin Romanov Gabriel Scherer Fr\u00e9d\u00e9ric Bour. 2020. TRMC reloaded. https:\/\/github.com\/ocaml\/ocaml\/pull\/9760  Konstantin Romanov Gabriel Scherer Fr\u00e9d\u00e9ric Bour. 2020. TRMC reloaded. https:\/\/github.com\/ocaml\/ocaml\/pull\/9760"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94205-6_42"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1238844.1238856"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_35"},{"key":"e_1_3_2_1_14_1","volume-title":"Programming Languages and Systems","author":"Jourdan Jacques-Henri","unstructured":"Jacques-Henri Jourdan , Fran\u00e7ois Pottier , and Xavier Leroy . 2012. Validating LR(1) Parsers . In Programming Languages and Systems . Springer Berlin Heidelberg , Berlin, Heidelberg . 397\u2013416. isbn:978-3-642-28869-2 Jacques-Henri Jourdan, Fran\u00e7ois Pottier, and Xavier Leroy. 2012. Validating LR(1) Parsers. In Programming Languages and Systems. Springer Berlin Heidelberg, Berlin, Heidelberg. 397\u2013416. isbn:978-3-642-28869-2"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94821-8_21"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_17"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2019.22"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040335"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-39185-1_12"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473579"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/FormaliSE.2019.00020"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/357084.357090"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_2"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/36177.36194"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167089"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.24"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364545"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/s0956796813000282"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00722-4_2"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679682100023X"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473591"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5075\/epfl-thesis-10285"},{"key":"e_1_3_2_1_36_1","unstructured":"Christine Paulin-Mohring. 1989. Extraction de programmes dans le Calcul des Constructions. Universit\u00e9 Paris-Diderot - Paris VII. https:\/\/tel.archives-ouvertes.fr\/tel-00431825  Christine Paulin-Mohring. 1989. Extraction de programmes dans le Calcul des Constructions. Universit\u00e9 Paris-Diderot - Paris VII. https:\/\/tel.archives-ouvertes.fr\/tel-00431825"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(06)80007-6"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594339"},{"key":"e_1_3_2_1_39_1","volume-title":"Relational compilation: Functional-to-imperative code generation for performance-critical applications","author":"Pit-Claudel Cl\u00e9ment","year":"2022","unstructured":"Cl\u00e9ment Pit-Claudel . 2022. Relational compilation: Functional-to-imperative code generation for performance-critical applications . Massachusetts Institute of Technology . https:\/\/pit-claudel.fr\/clement\/PhD\/RelationalCompilation_Pit-Claudel_ 2022 .pdf Cl\u00e9ment Pit-Claudel. 2022. Relational compilation: Functional-to-imperative code generation for performance-critical applications. Massachusetts Institute of Technology. https:\/\/pit-claudel.fr\/clement\/PhD\/RelationalCompilation_Pit-Claudel_2022.pdf"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6330740"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1_7"},{"key":"e_1_3_2_1_42_1","volume-title":"4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS","author":"Pnueli A.","year":"1998","unstructured":"A. Pnueli , M. Siegel , and E. Singerman . 1998. Translation validation . In 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 1998 ). Springer Berlin Heidelberg, Berlin, Heidelberg. 151\u2013166. isbn:978-3-540-69753-4 A. Pnueli, M. Siegel, and E. Singerman. 1998. Translation validation. In 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 1998). Springer Berlin Heidelberg, Berlin, Heidelberg. 151\u2013166. isbn:978-3-540-69753-4"},{"key":"e_1_3_2_1_43_1","volume-title":"Zero-cost meta-programmed stateful functors in F*. CoRR, abs\/2102.01644","author":"Protzenko Jonathan","year":"2021","unstructured":"Jonathan Protzenko and Son Ho. 2021. Zero-cost meta-programmed stateful functors in F*. CoRR, abs\/2102.01644 ( 2021 ), arxiv:2102.01644. arxiv:2102.01644 Jonathan Protzenko and Son Ho. 2021. Zero-cost meta-programmed stateful functors in F*. CoRR, abs\/2102.01644 (2021), arxiv:2102.01644. arxiv:2102.01644"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/sp40000.2020.00114"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110261"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454032"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-3794-8_16"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806611"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.4501022"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993514"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993533"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328444"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542512"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61464-8_50"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660201"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473589"},{"key":"e_1_3_2_1_58_1","volume-title":"5th International Workshop on Coq for PL (CoqPL","author":"Zaliva Vadim","year":"2019","unstructured":"Vadim Zaliva and Matthieu Sozeau . 2019 . Reification of shallow-embedded DSLs in Coq with automated verification . In 5th International Workshop on Coq for PL (CoqPL 2019). Vadim Zaliva and Matthieu Sozeau. 2019. Reification of shallow-embedded DSLs in Coq with automated verification. In 5th International Workshop on Coq for PL (CoqPL 2019)."}],"event":{"name":"PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation","location":"San Diego CA USA","acronym":"PLDI '22","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3519939.3523706","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3519939.3523706","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:10:30Z","timestamp":1750183830000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3519939.3523706"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6,9]]},"references-count":58,"alternative-id":["10.1145\/3519939.3523706","10.1145\/3519939"],"URL":"https:\/\/doi.org\/10.1145\/3519939.3523706","relation":{},"subject":[],"published":{"date-parts":[[2022,6,9]]},"assertion":[{"value":"2022-06-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}