{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T22:20:30Z","timestamp":1743114030063,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642038280"},{"type":"electronic","value":"9783642038297"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-03829-7_2","type":"book-chapter","created":{"date-parts":[[2009,8,10]],"date-time":"2009-08-10T05:05:20Z","timestamp":1249880720000},"page":"51-95","source":"Crossref","is-referenced-by-count":0,"title":["An Introduction to Certificate Translation"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[]},{"given":"C\u00e9sar","family":"Kunz","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-92188-2_1","volume-title":"Formal Methods for Components and Objects","author":"G. Barthe","year":"2008","unstructured":"Barthe, G., Cr\u00e9gut, P., Gr\u00e9goire, B., Jensen, T., Pichardie, D.: The MOBIUS proof carrying code infrastructure. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol.\u00a05382, pp. 1\u201324. Springer, Heidelberg (2008)"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/11823230_20","volume-title":"Static Analysis","author":"G. Barthe","year":"2006","unstructured":"Barthe, G., Gr\u00e9goire, B., Kunz, C., Rezk, T.: Certificate\u00a0translation\u00a0for\u00a0optimizing\u00a0compilers. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 301\u2013317. Springer, Heidelberg (2006)"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., Kunz, C., Rezk, T.: Certificate translation for optimizing compilers. ACM Transactions on Programming Languages and Systems (2009); Extended version of [2]","DOI":"10.1145\/1538917.1538919"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-540-78739-6_28","volume-title":"Programming Languages and Systems","author":"G. Barthe","year":"2008","unstructured":"Barthe, G., Kunz, C.: Certificate\u00a0translation\u00a0in\u00a0abstract\u00a0interpretation. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol.\u00a04960, pp. 368\u2013382. Springer, Heidelberg (2008)"},{"key":"2_CR5","volume-title":"Software Engineering and Formal Methods","author":"G. Barthe","year":"2008","unstructured":"Barthe, G., Kunz, C., Pichardie, D., Samborski-Forlese, J.: Preservation of proof obligations for hybrid verification methods. In: Software Engineering and Formal Methods. IEEE Press, Los Alamitos (2008)"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-540-45236-2_24","volume-title":"FME 2003: Formal Methods","author":"L. Burdy","year":"2003","unstructured":"Burdy, L., Requet, A., Lanet, J.-L.: Java applet correctness: A developer-oriented approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 422\u2013439. Springer, Heidelberg (2003)"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-30569-9_6","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"D.R. Cok","year":"2005","unstructured":"Cok, D.R., Kiniry, J.R.: ESC\/Java2: Uniting ESC\/Java and JML: Progress and issues in building and using esc\/java2 and a report on a case study involving the use of esc\/java2 to verify portions of an internet voting tally system. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 108\u2013128. Springer, Heidelberg (2005)"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principles of Programming Languages, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Principles of Programming Languages, pp. 269\u2013282 (1979)","DOI":"10.1145\/567752.567778"},{"key":"2_CR10","unstructured":"Darvas, \u00c1., M\u00fcller, P.: Formal encoding of JML level 0 specifications in jive. Technical report, ETH Zurich, Annual Report of the Chair of Software Engineering (2007)"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Proc. Symp. Appl. Math., vol.\u00a019, pp. 19\u201331 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"issue":"10","key":"2_CR12","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Communications of the ACM"},{"key":"2_CR13","first-page":"479","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"W.A. Howard","year":"1980","unstructured":"Howard, W.A.: The Formulae-As-Types Notion Of Construction. In: Seldin, J.P., Hindley, J.R. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 479\u2013490. Academic Press, Inc., New York (1980)"},{"key":"2_CR14","first-page":"42","volume-title":"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: Morrisett, J.G., Peyton Jones, S.L. (eds.) Principles of Programming Languages, pp. 42\u201354. ACM Press, New York (2006)"},{"key":"2_CR15","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.jlap.2003.07.006","volume":"58","author":"C. March\u00e9","year":"2004","unstructured":"March\u00e9, C., Paulin-Mohring, C., Urbain, X.: The Krakatoa tool for certification of Java\/JavaCard programs annotated with JML annotations. Journal of Logic and Algebraic Programming\u00a058, 89\u2013106 (2004)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"2_CR16","first-page":"106","volume-title":"Principles of Programming Languages","author":"G.C. Necula","year":"1997","unstructured":"Necula, G.C.: Proof-carrying code. In: Principles of Programming Languages, pp. 106\u2013119. ACM Press, New York (1997)"},{"issue":"5","key":"2_CR17","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1145\/358438.349314","volume":"35","author":"G.C. Necula","year":"2000","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. ACM SIGPLAN Notices\u00a035(5), 83\u201394 (2000)","journal-title":"ACM SIGPLAN Notices"},{"key":"2_CR18","first-page":"333","volume-title":"Programming Languages Design and Implementation","author":"G.C. Necula","year":"1998","unstructured":"Necula, G.C., Lee, P.: The design and implementation of a certifying compiler. In: Programming Languages Design and Implementation, vol.\u00a033, pp. 333\u2013344. ACM Press, New York (1998)"},{"key":"2_CR19","unstructured":"Necula, G.C.: Compiling with Proofs. PhD thesis, Carnegie Mellon University, Available as Technical Report CMU-CS-98-154 (October 1998)"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BFb0054170","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"1998","unstructured":"Pnueli, A., Singerman, E., Siegel, M.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 151\u2013166. Springer, Heidelberg (1998)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Security Analysis and Design V"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03829-7_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T12:10:29Z","timestamp":1558267829000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03829-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642038280","9783642038297"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03829-7_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}