{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:24:32Z","timestamp":1750220672686,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":13,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,1,17]],"date-time":"2021-01-17T00:00:00Z","timestamp":1610841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["20203001"],"award-info":[{"award-number":["20203001"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,1,18]]},"DOI":"10.1145\/3441296.3441394","type":"proceedings-article","created":{"date-parts":[[2020,12,23]],"date-time":"2020-12-23T00:32:44Z","timestamp":1608683564000},"page":"14-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Coq to C translation with partial evaluation"],"prefix":"10.1145","author":[{"given":"Akira","family":"Tanaka","sequence":"first","affiliation":[{"name":"AIST, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,1,17]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"The Third International Workshop on Coq for Programming Languages (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 The Third International Workshop on Coq for Programming Languages (CoqPL). 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 The Third International Workshop on Coq for Programming Languages (CoqPL)."},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237771"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2005.02.002"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155113"},{"key":"#cr-split#-e_1_3_2_2_5_1.1","doi-asserted-by":"crossref","unstructured":"Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM 52 7 ( 2009 ) 107-115. htps:\/\/doi.org\/10.1145\/1538788.1538814 10.1145\/1538788.1538814","DOI":"10.1145\/1538788.1538814"},{"key":"#cr-split#-e_1_3_2_2_5_1.2","doi-asserted-by":"crossref","unstructured":"Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM 52 7 ( 2009 ) 107-115. htps:\/\/doi.org\/10.1145\/1538788.1538814","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_2_6_1","volume-title":"Second International Workshop, TYPES 2002","author":"Letouzey Pierre","year":"2003","unstructured":"Pierre Letouzey . 2003 . A New Extraction for Coq. In Types for Proofs and Programs , Second International Workshop, TYPES 2002 , Berg en Dal, The Netherlands , April 24-28, 2002 (Lecture Notes in Computer Science, Vol. 2646 ), Herman Geuvers and Freek Wiedijk (Eds.). Springer-Verlag. htps:\/\/doi.org\/10.1007\/3-540-39185-1_12 10.1007\/3-540-39185-1_12 Pierre Letouzey. 2003. A New Extraction for Coq. In Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002 (Lecture Notes in Computer Science, Vol. 2646 ), Herman Geuvers and Freek Wiedijk (Eds.). Springer-Verlag. htps:\/\/doi.org\/10.1007\/3-540-39185-1_12"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167089"},{"volume-title":"Compact data structures: A practical approach","author":"Navarro Gonzalo","key":"e_1_3_2_2_8_1","unstructured":"Gonzalo Navarro . 2016. Compact data structures: A practical approach . Cambridge University Press . htps:\/\/doi.org\/10.1017\/ CBO9781316588284 Gonzalo Navarro. 2016. Compact data structures: A practical approach. Cambridge University Press. htps:\/\/doi.org\/10.1017\/ CBO9781316588284"},{"key":"#cr-split#-e_1_3_2_2_9_1.1","doi-asserted-by":"crossref","unstructured":"Akira Tanaka Reynald Afeldt and Jacques Garrigue. 2018. Safe lowlevel code generation in Coq using monomorphization and monadification. Journal of Information Processing 26 ( 2018 ) 54-72. htps: \/\/doi.org\/10.2197\/ipsjjip.26.54 10.2197\/ipsjjip.26.54","DOI":"10.2197\/ipsjjip.26.54"},{"key":"#cr-split#-e_1_3_2_2_9_1.2","doi-asserted-by":"crossref","unstructured":"Akira Tanaka Reynald Afeldt and Jacques Garrigue. 2018. Safe lowlevel code generation in Coq using monomorphization and monadification. Journal of Information Processing 26 ( 2018 ) 54-72. htps: \/\/doi.org\/10.2197\/ipsjjip.26.54","DOI":"10.2197\/ipsjjip.26.54"},{"key":"e_1_3_2_2_10_1","unstructured":"The Coq Development Team. 2020. The Coq Proof Assistant. htps: \/\/coq.inria.fr\/.  The Coq Development Team. 2020. The Coq Proof Assistant. htps: \/\/coq.inria.fr\/."},{"key":"e_1_3_2_2_11_1","first-page":"12","article-title":"The Coq reference manual","volume":"8","author":"Development Team The Coq","year":"2020","unstructured":"The Coq Development Team . 2020 . The Coq reference manual : Release 8. 12 .0. ( 2020 ). The Coq Development Team. 2020. The Coq reference manual: Release 8. 12.0. ( 2020 ).","journal-title":"Release"}],"event":{"name":"POPL '21: The 48th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Virtual Denmark","acronym":"POPL '21"},"container-title":["Proceedings of the 2021 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3441296.3441394","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3441296.3441394","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:03:04Z","timestamp":1750197784000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3441296.3441394"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,17]]},"references-count":13,"alternative-id":["10.1145\/3441296.3441394","10.1145\/3441296"],"URL":"https:\/\/doi.org\/10.1145\/3441296.3441394","relation":{},"subject":[],"published":{"date-parts":[[2021,1,17]]},"assertion":[{"value":"2021-01-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}