{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:14:55Z","timestamp":1775873695891,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":16,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,1,11]],"date-time":"2014-01-11T00:00:00Z","timestamp":1389398400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2014,1,11]]},"DOI":"10.1145\/2541568.2541572","type":"proceedings-article","created":{"date-parts":[[2014,1,14]],"date-time":"2014-01-14T13:40:06Z","timestamp":1389706806000},"page":"41-46","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Formalizing a correctness property of a type-directed partial evaluator"],"prefix":"10.1145","author":[{"given":"Noriko","family":"Hirota","sequence":"first","affiliation":[{"name":"Ochanomizu University, 2-1-1 Otsuka, Bunkyo-ku, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kenichi","family":"Asai","sequence":"additional","affiliation":[{"name":"Ochanomizu University, 2-1-1 Otsuka, Bunkyo-ku, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964007"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411226"},{"key":"e_1_3_2_1_3_1","unstructured":"Chlipala A. Certified Programming with Dependent Types available from http:\/\/adam.chlipala.net\/cpdt\/.  Chlipala A. Certified Programming with Dependent Types available from http:\/\/adam.chlipala.net\/cpdt\/."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1019964114625"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91622"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237784"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/645815.668894"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Filinski A. \"Normalization by Evaluation for the Computational Lambda-Calculus \" In S. Abramsky editor Typed Lambda Calculi and Applications (LNCS 2044) pp. 151--165 (May 2001).   Filinski A. \"Normalization by Evaluation for the Computational Lambda-Calculus \" In S. Abramsky editor Typed Lambda Calculi and Applications (LNCS 2044) pp. 151--165 (May 2001).","DOI":"10.1007\/3-540-45413-6_15"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/571157.571161"},{"key":"e_1_3_2_1_10_1","unstructured":"Ilik D. Constructive Completeness Proofs and Delimited Control Ph.D. thesis Ecole Polytechnique X (October 2010).  Ilik D. Constructive Completeness Proofs and Delimited Control Ph.D. thesis Ecole Polytechnique X (October 2010)."},{"key":"e_1_3_2_1_11_1","article-title":"Continuation-passing style models complete for intuitionistic logic","author":"Ilik D.","year":"2010","journal-title":"Annals of Pure and Applied Logic, Special issue: Classical logic and computation"},{"key":"e_1_3_2_1_12_1","unstructured":"Ilik D. \"A formalized type-directed partial evaluator for shift and reset\" Control Operators and their Semantics available from http:\/\/arxiv.org\/abs\/1210.2094 18 pages (April 2013).  Ilik D. \"A formalized type-directed partial evaluator for shift and reset\" Control Operators and their Semantics available from http:\/\/arxiv.org\/abs\/1210.2094 18 pages (April 2013)."},{"key":"e_1_3_2_1_13_1","unstructured":"Jones N. D. C. K. Gomard and P. Sestoft Partial Evaluation and Automatic Program Generation New York: Prentice-Hall (1993).   Jones N. D. C. K. Gomard and P. Sestoft Partial Evaluation and Automatic Program Generation New York: Prentice-Hall (1993)."},{"key":"e_1_3_2_1_14_1","unstructured":"Lindley S. Normalisation by Evaluation in the Compilation of TypedFunctional Programming Languages Ph.D. thesis University of Edinburgh (2005).  Lindley S. Normalisation by Evaluation in the Compilation of TypedFunctional Programming Languages Ph.D. thesis University of Edinburgh (2005)."},{"key":"e_1_3_2_1_15_1","first-page":"57","volume-title":"Proceedings of the 2009 Workshop on Normalization by Evaluation","author":"Tsushima K.","year":"2009"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006557"}],"event":{"name":"POPL '14: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"San Diego California USA","acronym":"POPL '14","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the ACM SIGPLAN 2014 Workshop on Programming Languages meets Program Verification"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2541568.2541572","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2541568.2541572","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:35:02Z","timestamp":1750232102000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2541568.2541572"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,1,11]]},"references-count":16,"alternative-id":["10.1145\/2541568.2541572","10.1145\/2541568"],"URL":"https:\/\/doi.org\/10.1145\/2541568.2541572","relation":{},"subject":[],"published":{"date-parts":[[2014,1,11]]},"assertion":[{"value":"2014-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}