{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:02:19Z","timestamp":1760043739412},"reference-count":15,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2008,1,12]],"date-time":"2008-01-12T00:00:00Z","timestamp":1200096000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2008,5]]},"DOI":"10.1007\/s10817-007-9096-8","type":"journal-article","created":{"date-parts":[[2008,1,11]],"date-time":"2008-01-11T09:03:34Z","timestamp":1200042214000},"page":"307-326","source":"Crossref","is-referenced-by-count":14,"title":["Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves"],"prefix":"10.1007","volume":"40","author":[{"given":"Laurence","family":"Rideau","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernard Paul","family":"Serpette","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xavier","family":"Leroy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2008,1,12]]},"reference":[{"key":"9096_CR1","doi-asserted-by":"crossref","unstructured":"Appel, A.W.: Compiling with Continuations. Cambridge University Press (1992)","DOI":"10.1017\/CBO9780511609619"},{"key":"9096_CR2","unstructured":"Balaa, A., Bertot, Y.: Fonctions r\u00e9cursives g\u00e9n\u00e9rales par it\u00e9ration en th\u00e9orie des types. In: Journ\u00e9es Francophones des Langages Applicatifs 2002, pp. 27\u201342. INRIA (2002)"},{"key":"9096_CR3","doi-asserted-by":"crossref","unstructured":"Barthe, G., Forest, J., Pichardie, D., Rusu, V.: Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant. In: Proceedings of the 8th International Symposium on Functional and Logic Programming (FLOPS\u201906). Lecture Notes in Computer Science, vol. 3945, pp.\u00a0114\u2013129. Springer (2006)","DOI":"10.1007\/11737414_9"},{"key":"9096_CR4","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive theorem proving and program development\u2014Coq\u2019Art: the calculus of inductive constructions. EATCS Texts in Theoretical Computer Science. Springer (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"9096_CR5","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Gr\u00e9goire, B., Leroy, X.: A structured approach to proving compiler optimizations based on dataflow analysis. In: Types for Proofs and Programs, Workshop TYPES 2004. Lecture Notes in Computer Science, vol. 3839, pp. 66\u201381. Springer (2006)","DOI":"10.1007\/11617990_5"},{"key":"9096_CR6","doi-asserted-by":"crossref","unstructured":"Blazy, S., Dargaye, Z., Leroy, X.: Formal verification of a C compiler front-end. In: FM 2006: International Symposium on Formal Methods. Lecture Notes in Computer Science, vol. 4085, pp. 460\u2013475. Springer (2006)","DOI":"10.1007\/11813040_31"},{"key":"9096_CR7","unstructured":"Coq Development Team: the Coq proof assistant. Software and documentation available at http:\/\/coq.inria.fr\/ (1989\u20132007)"},{"issue":"4","key":"9096_CR8","doi-asserted-by":"crossref","first-page":"709","DOI":"10.1017\/S095679680200446X","volume":"13","author":"J.C. Filli\u00e2tre","year":"2003","unstructured":"Filli\u00e2tre, J.C.: Verification of non-functional programs using interpretations in type theory. J. Funct. Program. 13(4), 709\u2013745 (2003)","journal-title":"J. Funct. Program."},{"key":"9096_CR9","unstructured":"Filli\u00e2tre, J.C.: The Why software verification tool. Software and documentation available at http:\/\/why.lri.fr\/ (2003\u20132007)"},{"key":"9096_CR10","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: 33rd Symposium Principles of Programming Languages, pp. 42\u201354. ACM Press (2006)","DOI":"10.1145\/1111037.1111042"},{"key":"9096_CR11","unstructured":"Leroy, X., Doligez, D., Garrigue, J., Vouillon, J.: The Objective Caml system. Software and documentation available at http:\/\/caml.inria.fr\/ (1996\u20132007)"},{"key":"9096_CR12","doi-asserted-by":"crossref","unstructured":"Letouzey, P.: A new extraction for Coq. In: Types for Proofs and Programs, Workshop TYPES 2002. Lecture Notes in Computer Science, vol. 2646, pp. 200\u2013219. Springer (2003)","DOI":"10.1007\/3-540-39185-1_12"},{"issue":"6","key":"9096_CR13","doi-asserted-by":"crossref","first-page":"821","DOI":"10.1109\/32.24735","volume":"15","author":"C. May","year":"1989","unstructured":"May, C.: The parallel assignment problem redefined. IEEE Trans. Softw. Eng. 15(6), 821\u2013824 (1989)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"4","key":"9096_CR14","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1016\/0020-0190(73)90024-0","volume":"2","author":"R. Sethi","year":"1973","unstructured":"Sethi, R.: A note on implementing parallel assignment instructions. Inf. Process. Lett. 2(4), 91\u201395 (1973)","journal-title":"Inf. Process. Lett."},{"issue":"12","key":"9096_CR15","doi-asserted-by":"crossref","first-page":"1175","DOI":"10.1002\/spe.4380131208","volume":"13","author":"P.H. Welch","year":"1983","unstructured":"Welch, P.H.: Parallel assignment revisited. Software Practice and Experience 13(12), 1175\u20131180 (1983)","journal-title":"Software Practice and Experience"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-007-9096-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-007-9096-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-007-9096-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T21:21:48Z","timestamp":1559251308000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-007-9096-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,1,12]]},"references-count":15,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2008,5]]}},"alternative-id":["9096"],"URL":"https:\/\/doi.org\/10.1007\/s10817-007-9096-8","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,1,12]]}}}