{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T20:56:13Z","timestamp":1768251373141,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540755586","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-75560-9_17","type":"book-chapter","created":{"date-parts":[[2007,10,6]],"date-time":"2007-10-06T05:36:46Z","timestamp":1191649006000},"page":"211-225","source":"Crossref","is-referenced-by-count":10,"title":["Mechanized Verification of CPS Transformations"],"prefix":"10.1007","author":[{"given":"Zaynah","family":"Dargaye","sequence":"first","affiliation":[]},{"given":"Xavier","family":"Leroy","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"4","key":"17_CR1","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., Cardelli, L., Curien, P.-L., L\u00e9vy, J.-J.: Explicit substitutions. Journal of Functional Programming\u00a01(4), 375\u2013416 (1991)","journal-title":"Journal of Functional Programming"},{"key":"17_CR2","volume-title":"Compiling with continuations","author":"A.W. Appel","year":"1992","unstructured":"Appel, A.W.: Compiling with continuations. Cambridge University Press, Cambridge (1992)"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/11541868_4","volume-title":"Theorem Proving in Higher Order Logics","author":"B.E. Aydemir","year":"2005","unstructured":"Aydemir, B.E., Bohannon, A., Fairbairn, M., Foster, J.N., Pierce, B.C., Sewell, P., Vytiniotis, D., Washburn, G., Weirich, S., Zdancewic, S.: Mechanized metatheory for the masses: The POPLmark challenge. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 50\u201365. Springer, Heidelberg (2005)"},{"key":"17_CR4","volume-title":"EATCS Texts in Theoretical Computer Science","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development \u2013 Coq\u2019Art: The Calculus of Inductive Constructions. In: EATCS Texts in Theoretical Computer Science, Springer, Heidelberg (2004)"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/11813040_31","volume-title":"FM 2006: Formal Methods","author":"S. Blazy","year":"2006","unstructured":"Blazy, S., Dargaye, Z., Leroy, X.: Formal verification of a C compiler front-end. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 460\u2013475. Springer, Heidelberg (2006)"},{"key":"17_CR6","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1145\/1250734.1250742","volume-title":"Programming Language Design and Implementation 2007","author":"A. Chlipala","year":"2007","unstructured":"Chlipala, A.: A certified type-preserving compiler from lambda calculus to assembly language. In: Programming Language Design and Implementation 2007, pp. 54\u201365. ACM Press, New York (2007)"},{"key":"17_CR7","unstructured":"Coq development team. The Coq proof assistant. Software and documentation (1989\u20132007), available at http:\/\/coq.inria.fr\/"},{"issue":"1-3","key":"17_CR8","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/S0304-3975(02)00733-8","volume":"308","author":"O. Danvy","year":"2003","unstructured":"Danvy, O., Nielsen, L.R.: A first-order one-pass CPS transformation. Theoretical Computer Science\u00a0308(1-3), 239\u2013257 (2003)","journal-title":"Theoretical Computer Science"},{"issue":"5","key":"17_CR9","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/j.ipl.2005.02.002","volume":"94","author":"O. Danvy","year":"2005","unstructured":"Danvy, O., Nielsen, L.R.: CPS transformation of beta-redexes. Information Processing Letters\u00a094(5), 217\u2013224 (2005)","journal-title":"Information Processing Letters"},{"key":"17_CR10","unstructured":"Dargaye, Z.: D\u00e9curryfication certifi\u00e9e. In: Journ\u00e9es Francophones des Langages Applicatifs (JFLA 2007), INRIA (2007)"},{"issue":"5","key":"17_CR11","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N.G. Bruijn de","year":"1972","unstructured":"de Bruijn, N.G.: Lambda-calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indag. Math.\u00a034(5), 381\u2013392 (1972)","journal-title":"Indag. Math."},{"key":"17_CR12","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1145\/155090.155113","volume-title":"Programming Language Design and Implementation 1993","author":"C. Flanagan","year":"1993","unstructured":"Flanagan, C., Sabry, A., Duba, B., Felleisen, M.: The essence of compiling with continuations. In: Programming Language Design and Implementation 1993, pp. 237\u2013247. ACM Press, New York (1993)"},{"key":"17_CR13","volume-title":"International Conference on Functional Programming","author":"A. Kennedy","year":"2007","unstructured":"Kennedy, A.: Compiling with continuations, continued. In: International Conference on Functional Programming, ACM Press, New York (2007)"},{"issue":"4","key":"17_CR14","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1145\/1146809.1146811","volume":"28","author":"G. Klein","year":"2006","unstructured":"Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. ACM Transactions on Programming Languages and Systems\u00a028(4), 619\u2013695 (2006)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"17_CR15","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1145\/12276.13333","volume-title":"SIGPLAN 1986","author":"D. Kranz","year":"1986","unstructured":"Kranz, D., Adams, N., Kelsey, R., Rees, J., Hudak, P., Philbin, J.: ORBIT: an optimizing compiler for Scheme. In: SIGPLAN 1986. symposium on Compiler Construction, pp. 219\u2013233. ACM Press, New York (1986)"},{"key":"17_CR16","first-page":"2","volume-title":"SEFM 2005","author":"D. Leinenbach","year":"2005","unstructured":"Leinenbach, D., Paul, W., Petrova, E.: Towards the formal verification of a C0 compiler: Code generation and implementation correctness. In: SEFM 2005. Int. Conf. on Software Engineering and Formal Methods, pp. 2\u201311. IEEE Computer Society Press, Los Alamitos (2005)"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/11693024_5","volume-title":"Programming Languages and Systems","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Coinductive big-step operational semantics. In: Sestoft, P. (ed.) ESOP 2006 and ETAPS 2006. LNCS, vol.\u00a03924, pp. 54\u201368. Springer, Heidelberg (2006)"},{"key":"17_CR18","first-page":"42","volume-title":"33rd symposium Principles of Programming Languages","author":"X. Leroy","year":"2006","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, New York (2006)"},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-39185-1_12","volume-title":"Types for Proofs and Programs","author":"P. Letouzey","year":"2003","unstructured":"Letouzey, P.: A new extraction for Coq. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol.\u00a02646, pp. 200\u2013219. Springer, Heidelberg (2003)"},{"key":"17_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/976571.976576","volume-title":"MERLIN 2003","author":"Y. Minamide","year":"2003","unstructured":"Minamide, Y., Okuma, K.: Verifying CPS transformations in Isabelle\/HOL. In: MERLIN 2003. Proc. workshop on Mechanized reasoning about languages with variable binding, pp. 1\u20138. ACM Press, New York (2003)"},{"key":"17_CR21","volume-title":"Piton: a mechanically verified assembly-language","author":"J.S. Moore","year":"1996","unstructured":"Moore, J.S.: Piton: a mechanically verified assembly-language. Kluwer Academic Publishers, Dordrecht (1996)"},{"issue":"2","key":"17_CR22","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"G.D. Plotkin","year":"1975","unstructured":"Plotkin, G.D.: Call-by-name, call-by-value and the lambda-calculus. Theoretical Computer Science\u00a01(2), 125\u2013159 (1975)","journal-title":"Theoretical Computer Science"},{"issue":"6","key":"17_CR23","doi-asserted-by":"publisher","first-page":"916","DOI":"10.1145\/267959.269968","volume":"19","author":"A. Sabry","year":"1997","unstructured":"Sabry, A., Wadler, P.: A reflection on call-by-value. ACM Transactions on Programming Languages and Systems\u00a019(6), 916\u2013941 (1997)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"17_CR24","unstructured":"Tian, Y.H.: Mechanically verifying correctness of CPS compilation. In: CATS 2006. Proceedings of the 12th Computing: The Australasian Theory Symposium, pp. 41\u201351. Australian Computer Society (2006)"},{"key":"17_CR25","doi-asserted-by":"crossref","unstructured":"Urban, C.: Nominal techniques in Isabelle\/HOL. Journal of Automated Reasoning (to appear, 2007)","DOI":"10.1007\/s10817-008-9097-2"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75560-9_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:24:40Z","timestamp":1619519080000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75560-9_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540755586"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75560-9_17","relation":{},"subject":[]}}