{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,15]],"date-time":"2026-08-15T04:27:28Z","timestamp":1786768048434,"version":"build-2736575974"},"reference-count":14,"publisher":"Information Processing Society of Japan","issue":"0","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Information Processing"],"published-print":{"date-parts":[[2026]]},"DOI":"10.2197\/ipsjjip.34.656","type":"journal-article","created":{"date-parts":[[2026,8,14]],"date-time":"2026-08-14T22:10:42Z","timestamp":1786745442000},"page":"656-670","source":"Crossref","is-referenced-by-count":0,"title":["Verified Gallina Transformations in the Codegen Plugin for Rocq"],"prefix":"10.2197","volume":"34","author":[{"given":"Akira","family":"Tanaka","sequence":"first","affiliation":[{"name":"Intelligent Platforms Research Institute, National Institute of Advanced Industrial Science and Technology (AIST)"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"1012","reference":[{"key":"1","unstructured":"[1] Anand, A., Appel, A., Morrisett, G., Paraskevopoulou, Z., Pollack, R., Belanger, O.S., Sozeau, M. and Weaver, M.: CertiCoq: A verified compiler for Coq, <i>The 3rd International Workshop on Coq for Programming Languages<\/i> (<i>CoqPL<\/i>) (2017)."},{"key":"2","doi-asserted-by":"crossref","unstructured":"[2] Barthe, G. and Courtieu, P.: Efficient reasoning about executable specifications in Coq, <i>International Conference on Theorem Proving in Higher Order Logics<\/i>, pp.31-46, Springer (2002).","DOI":"10.1007\/3-540-45685-6_4"},{"key":"3","unstructured":"[3] Bertot, Y. and Cast\u00e9ran, P.: <i>Interactive theorem proving and program development: Coq&apos;Art: The calculus of inductive constructions<\/i>, Springer Science &amp; Business Media (2013)."},{"key":"4","doi-asserted-by":"crossref","unstructured":"[4] Flanagan, C., Sabry, A., Duba, B.F. and Felleisen, M.: The essence of compiling with continuations, <i>Proc. ACM SIGPLAN 1993 Conference on Programming Language Design and Implementation<\/i>, pp.237-247 (online), DOI: 10.1145\/155090.155113 (1993).","DOI":"10.1145\/155090.155113"},{"key":"5","doi-asserted-by":"crossref","unstructured":"[5] Forster, Y., Sozeau, M. and Tabareau, N.: Verified extraction from coq to ocaml, <i>Proc. ACM on Programming Languages<\/i>, Vol.8, No.PLDI, pp.52-75 (2024).","DOI":"10.1145\/3656379"},{"key":"6","doi-asserted-by":"crossref","unstructured":"[6] Letouzey, P.: A New Extraction for Coq, <i>Types for Proofs and Programs, 2nd International Workshop, TYPES 2002<\/i>, Geuvers, H. and Wiedijk, F. (Eds.), Lecture Notes in Computer Science, Vol.2646, Springer-Verlag (online), DOI: 10.1007\/3-540-39185-1_12 (2003).","DOI":"10.1007\/3-540-39185-1_12"},{"key":"7","unstructured":"[7] Mathematical Components organization: Mathematical Components (2025), available from &lt;https:\/\/math-comp.github.io\/&gt;."},{"key":"8","doi-asserted-by":"crossref","unstructured":"[8] Mullen, E., Pernsteiner, S., Wilcox, J.R., Tatlock, Z. and Grossman, D.: \u0152uf: Minimizing the Coq extraction TCB, <i>Proc. 7th ACM SIGPLAN International Conference on Certified Programs and Proofs<\/i>, pp.172-185 (online), DOI: 10.1145\/3167089 (2018).","DOI":"10.1145\/3167089"},{"key":"9","doi-asserted-by":"crossref","unstructured":"[9] Sozeau, M., Anand, A., Boulier, S., Cohen, C., Forster, Y., Kunze, F., Malecha, G., Tabareau, N. and Winterhalter, T.: The metacoq project, <i>Journal of Automated Reasoning<\/i>, Vol.64, No.5, pp.947-999 (2020).","DOI":"10.1007\/s10817-019-09540-0"},{"key":"10","doi-asserted-by":"crossref","unstructured":"[10] Steele, G.L.: It&apos;s Time for a New Old Language, <i>Proc. 22nd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP &apos;17<\/i>, p.1, Association for Computing Machinery (online), DOI: 10.1145\/3018743.3018773 (2017), available from &lt;https:\/\/labs.oracle.com\/pls\/apex\/f?p=94065:10:175964141145:4986&gt;.","DOI":"10.1145\/3018743.3018773"},{"key":"11","doi-asserted-by":"crossref","unstructured":"[11] Tanaka, A.: Coq to C translation with partial evaluation, <i>Proc. 2021 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation<\/i> (<i>PEPM<\/i>), pp.14-31 (online), DOI: 10.1145\/3441296.3441394(2021).","DOI":"10.1145\/3441296.3441394"},{"key":"12","unstructured":"[12] The Rocq Development Team: Rocq Reference Manual: Release 9.1.0 (2025) (online), available from &lt;https:\/\/rocq-prover.org\/doc\/V9.1.0\/refman\/index.html&gt;."},{"key":"13","unstructured":"[13] The Rocq Development Team: The Rocq Proof Assistant (2025), available from &lt;https:\/\/rocq-prover.org\/&gt;."},{"key":"14","unstructured":"[14] yannl35133: Proof of False because of guard checker (2025), available from &lt;https:\/\/github.com\/rocq-prover\/rocq\/issues\/20455&gt;."}],"container-title":["Journal of Information Processing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/ipsjjip\/34\/0\/34_656\/_pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,15]],"date-time":"2026-08-15T03:49:09Z","timestamp":1786765749000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/ipsjjip\/34\/0\/34_656\/_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"references-count":14,"journal-issue":{"issue":"0","published-print":{"date-parts":[[2026]]}},"URL":"https:\/\/doi.org\/10.2197\/ipsjjip.34.656","relation":{},"ISSN":["1882-6652"],"issn-type":[{"value":"1882-6652","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]}}}