{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T12:48:31Z","timestamp":1725540511920},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642103728"},{"type":"electronic","value":"9783642103735"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-10373-5_28","type":"book-chapter","created":{"date-parts":[[2009,11,16]],"date-time":"2009-11-16T11:45:27Z","timestamp":1258371927000},"page":"541-560","source":"Crossref","is-referenced-by-count":3,"title":["Implementing a Direct Method for Certificate Translation"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[]},{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[]},{"given":"Sylvain","family":"Heraud","sequence":"additional","affiliation":[]},{"given":"C\u00e9sar","family":"Kunz","sequence":"additional","affiliation":[]},{"given":"Anne","family":"Pacalet","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"28_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"28_CR2","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 translation in abstract interpretation. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol.\u00a04960, pp. 368\u2013382. Springer, Heidelberg (2008)"},{"issue":"5","key":"28_CR3","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1145\/1538917.1538919","volume":"31","author":"G. Barthe","year":"2009","unstructured":"Barthe, G., Gr\u00e9goire, B., Kunz, C., Rezk, T.: Certificate translation for optimizing compilers. ACM Transactions on Programming Languages and Systems\u00a031(5), 18:1\u201318:45 (2009)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"28_CR4","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1145\/1375581.1375604","volume-title":"Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation","author":"J. Chen","year":"2008","unstructured":"Chen, J., Hawblitzel, C., Perry, F., Emmi, M., Condit, J., Coetzee, D., Pratikakis, P.: Type-preserving compilation for large-scale optimizing object-oriented compilers. In: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, pp. 183\u2013192. ACM, New York (2008)"},{"key":"28_CR5","unstructured":"Monate, B., Correnson, L.: Frama-C, \n                    \n                      http:\/\/frama-c.cea.fr"},{"issue":"3","key":"28_CR6","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1145\/319301.319345","volume":"21","author":"G. Morrisett","year":"1999","unstructured":"Morrisett, G., Walker, D., Crary, K., Glew, N.: From system F to typed assembly language. ACM Transactions on Programming Languages and Systems\u00a021(3), 527\u2013568 (1999); Expanded version of a paper presented at POPL 1998 (1998)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"28_CR7","unstructured":"Necula, G.C.: Compiling with Proofs. PhD thesis, Carnegie Mellon University, Available as Technical Report CMU-CS-98-154 (October 1998)"},{"key":"28_CR8","series-title":"LNBIP","volume-title":"TOOLS-EUROPE","author":"M. Nordio","year":"2008","unstructured":"Nordio, M., M\u00fcller, P., Meyer, B.: Proof-transforming compilation of eiffel programs. In: Paige, R. (ed.) TOOLS-EUROPE. LNBIP. Springer, Heidelberg (2008)"},{"key":"28_CR9","unstructured":"Pavlova, M.: Java bytecode verification and its applications. Th\u00e8se de doctorat, sp\u00e9cialit\u00e9 informatique, Universit\u00e9 Nice Sophia Antipolis, France (January 2007)"},{"issue":"6","key":"28_CR10","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1145\/1286821.1286830","volume":"29","author":"S. Seo","year":"2007","unstructured":"Seo, S., Yang, H., Yi, K., Han, T.: Goal-directed weakening of abstract interpretation results. ACM Transactions on Programming Languages and Systems\u00a029(6), 39:1\u201339:39 (2007)","journal-title":"ACM Transactions on Programming Languages and Systems"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-10373-5_28.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T11:28:52Z","timestamp":1619782132000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-10373-5_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642103728","9783642103735"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-10373-5_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}