{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:29:40Z","timestamp":1761596980556},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540377566"},{"type":"electronic","value":"9783540377580"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11823230_20","type":"book-chapter","created":{"date-parts":[[2006,8,17]],"date-time":"2006-08-17T13:46:30Z","timestamp":1155822390000},"page":"301-317","source":"Crossref","is-referenced-by-count":18,"title":["Certificate\u00a0Translation\u00a0for\u00a0Optimizing\u00a0Compilers"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[]},{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[]},{"given":"C\u00e9sar","family":"Kunz","sequence":"additional","affiliation":[]},{"given":"Tamara","family":"Rezk","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Proceedings of Bytecode 2005","author":"F. Bannwart","year":"2005","unstructured":"Bannwart, F., M\u00fcller, P.: A program logic for bytecode. In: Spoto, F. (ed.) Proceedings of Bytecode 2005. Electronic Notes in Theoretical Computer Science. Elsevier Publishing, Amsterdam (2005)"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# Programming System: An Overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/11679219_9","volume-title":"Formal Aspects in Security and Trust","author":"G. Barthe","year":"2006","unstructured":"Barthe, G., Rezk, T., Saabas, A.: Proof obligations preserving compilation. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2005. LNCS, vol.\u00a03866, pp. 112\u2013126. Springer, Heidelberg (2006)"},{"key":"20_CR4","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/964001.964003","volume-title":"Proceedings of POPL 2004","author":"N. Benton","year":"2004","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: Proceedings of POPL 2004, pp. 14\u201325. ACM Press, New York (2004)"},{"key":"20_CR5","volume-title":"Proceedings of SAC 2006","author":"L. Burdy","year":"2006","unstructured":"Burdy, L., Pavlova, M.: Annotation carrying code. In: Proceedings of SAC 2006. ACM Press, New York (2006)"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Guttman, J.D., Wand, M.: Special issue on VLISP. Lisp and Symbolic Computation\u00a08(1\/2) (March 1995)","DOI":"10.1007\/BF01128406"},{"key":"20_CR7","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1145\/1040305.1040335","volume-title":"Proceedings of POPL 2005","author":"S. Lerner","year":"2005","unstructured":"Lerner, S., Millstein, T., Rice, E., Chambers, C.: Automated soundness proofs for dataflow analyses and transformations via local rules. In: Proceedings of POPL 2005, pp. 364\u2013377. ACM Press, New York (2005)"},{"key":"20_CR8","first-page":"42","volume-title":"Proceedings of POPL 2006","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Proceedings of POPL 2006, pp. 42\u201354. ACM Press, New York (2006)"},{"key":"20_CR9","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1145\/263699.263712","volume-title":"Proceedings of POPL 1997","author":"G.C. Necula","year":"1997","unstructured":"Necula, G.C.: Proof-Carrying Code. In: Proceedings of POPL 1997, pp. 106\u2013119. ACM Press, New York (1997)"},{"key":"20_CR10","unstructured":"Necula, G.C.: Compiling with Proofs. PhD thesis, Carnegie Mellon University, Available as Technical Report CMU-CS-98-154 (October 1998)"},{"key":"20_CR11","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1145\/277650.277752","volume-title":"Proceedings of PLDI 1998","author":"G.C. Necula","year":"1998","unstructured":"Necula, G.C., Lee, P.: The Design and Implementation of a Certifying Compiler. In: Proceedings of PLDI 1998, pp. 333\u2013344. ACM Press, New York (1998)"},{"key":"20_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-540-40018-9_16","volume-title":"Programming Languages and Systems","author":"S. Seo","year":"2003","unstructured":"Seo, S., Yang, H., Yi, K.: Automatic Construction of Hoare Proofs from Abstract Interpretation Results. In: Ohori, A. (ed.) APLAS 2003. LNCS, vol.\u00a02895, pp. 230\u2013245. Springer, Heidelberg (2003)"},{"key":"20_CR13","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Proceedings of BYTECODE 2005","author":"M. Wildmoser","year":"2005","unstructured":"Wildmoser, M., Chaieb, A., Nipkow, T.: Bytecode analysis for proof carrying code. In: Spoto, F. (ed.) Proceedings of BYTECODE 2005. Electronic Notes in Theoretical Computer Science. Elsevier Publishing, Amsterdam (2005)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11823230_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:17:03Z","timestamp":1605644223000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11823230_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540377566","9783540377580"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/11823230_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}