{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T11:38:19Z","timestamp":1725536299689},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642033582"},{"type":"electronic","value":"9783642033599"}],"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-03359-9_15","type":"book-chapter","created":{"date-parts":[[2009,8,20]],"date-time":"2009-08-20T01:46:12Z","timestamp":1250732772000},"page":"196-211","source":"Crossref","is-referenced-by-count":3,"title":["Formal Certification of a Resource-Aware Language Implementation"],"prefix":"10.1007","author":[{"given":"Javier","family":"de Dios","sequence":"first","affiliation":[]},{"given":"Ricardo","family":"Pe\u00f1a","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/3-540-45294-X_13","volume-title":"FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science","author":"A. Dold","year":"2001","unstructured":"Dold, A., Vialard, V.: A Mechanically Verified Compiling Specification for a Lisp Compiler. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol.\u00a02245, pp. 144\u2013155. Springer, Heidelberg (2001)"},{"key":"15_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 Translation for Optimizing Compilers. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 301\u2013317. Springer, Heidelberg (2006)"},{"key":"15_CR3","unstructured":"Berghofer, S., Strecker, M.: Extracting a formally verified, fully executable compiler from a proof assistant. In: Proc. Compiler Optimization Meets Compiler Verification, COCV 2003. ENTCS, pp. 33\u201350 (2003)"},{"key":"15_CR4","series-title":"Texts in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004)"},{"key":"15_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)"},{"issue":"6","key":"15_CR6","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/966221.966235","volume":"28","author":"M.A. Dave","year":"2003","unstructured":"Dave, M.A.: Compiler verification: a bibliography. SIGSOFT Software Engineering Notes\u00a028(6), 2 (2003)","journal-title":"SIGSOFT Software Engineering Notes"},{"key":"15_CR7","first-page":"185","volume-title":"Proc. 30th ACM Symp. on Principles of Programming Languages, POPL 2003","author":"M. Hofmann","year":"2003","unstructured":"Hofmann, M., Jost, S.: Static prediction of heap space usage for first-order functional programs. In: Proc. 30th ACM Symp. on Principles of Programming Languages, POPL 2003, pp. 185\u2013197. ACM Press, New York (2003)"},{"key":"15_CR8","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1016\/S0304-3975(02)00869-1","volume":"298","author":"G. Klein","year":"2003","unstructured":"Klein, G., Nipkow, T.: Verified Bytecode Verifiers. Theoretical Computer Science\u00a0298, 583\u2013626 (2003)","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"15_CR9","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":"15_CR10","first-page":"42","volume-title":"Principles of Programming Languages, 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: Principles of Programming Languages, POPL 2006, pp. 42\u201354. ACM Press, New York (2006)"},{"key":"15_CR11","unstructured":"Leroy, X.: A formally verified compiler back-end, July 2008, p. 79 (submitted, 2008)"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/978-3-540-71316-6_15","volume-title":"Programming Languages and Systems","author":"G. Li","year":"2007","unstructured":"Li, G., Owens, S., Slind, K.: Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 205\u2013219. Springer, Heidelberg (2007)"},{"key":"15_CR13","series-title":"The Java Series","volume-title":"The Java Virtual Machine Sepecification","author":"T. Lindholm","year":"1999","unstructured":"Lindholm, T., Yellin, F.: The Java Virtual Machine Sepecification, 2nd edn. The Java Series. Addison-Wesley, Reading (1999)","edition":"2"},{"key":"15_CR14","unstructured":"Montenegro, M., Pe\u00f1a, R., Segura, C.: A Resource-Aware Semantics and Abstract Machine for a Functional Language with Explicit Deallocation. In: Workshop on Functional and (Constraint) Logic Programming, WFLP 2008, Siena, Italy, July 2008, pp. 47\u201361 (2008) (to appear in ENTCS)"},{"key":"15_CR15","unstructured":"Montenegro, M., Pe\u00f1a, R., Segura, C.: A Simple Region Inference Algorithm for a First-Order Functional Language. In: Trends in Functional Programming, TFP 2008, Nijmegen (The Netherlands), May 2008, pp. 194\u2013208 (2008)"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Montenegro, M., Pe\u00f1a, R., Segura, C.: A Type System for Safe Memory Management and its Proof of Correctness. In: ACM Principles and Practice of Declarative Programming, PPDP 2008, Valencia, Spain, July 2008, pp. 152\u2013162 (2008)","DOI":"10.1145\/1389449.1389468"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/978-3-642-00515-2_10","volume-title":"LOPSTR 2008","author":"M. Montenegro","year":"2009","unstructured":"Montenegro, M., Pe\u00f1a, R., Segura, C.: An Inference Algorithm for Guaranteeing Safe Destruction. In: LOPSTR 2008. LNCS, vol.\u00a05438, pp. 135\u2013151. Springer, Heidelberg (2009)"},{"key":"15_CR18","first-page":"106","volume-title":"ACM SIGPLAN-SIGACT Principles of Programming Languages, POPL 1997","author":"G.C. Necula","year":"1997","unstructured":"Necula, G.C.: Proof-Carrying Code. In: ACM SIGPLAN-SIGACT Principles of Programming Languages, POPL 1997, pp. 106\u2013119. ACM Press, New York (1997)"},{"issue":"5","key":"15_CR19","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. SIGPLAN Notices\u00a035(5), 83\u201394 (2000)","journal-title":"SIGPLAN Notices"},{"key":"15_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL. A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL. A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"15_CR21","unstructured":"Pe\u00f1a, R., Rup\u00e9rez, D.: A Certified Implementation of a Functional Virtual Machine on top of the Java Virtual Machine. In: Jornadas sobre Programaci\u00f3n y Lenguajes, PROLE 2008, Gij\u00f3n, Spain, October 2008, pp. 131\u2013140 (2008)"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"Pe\u00f1a, R., Segura, C., Montenegro, M.: A Sharing Analysis for SAFE. In: Selected Papers of the 7th Symp. on Trends in Functional Programming, TFP 2006, pp. 109\u2013128 (2007) (Intellect)","DOI":"10.2307\/j.ctv36xvknz.10"},{"key":"15_CR23","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., Siegel, M., Singerman, E.: Translation Validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 151\u2013166. Springer, Heidelberg (1998)"},{"key":"15_CR24","unstructured":"Sannela, D., Hofmann, M.: Mobile Resources Guarantees. EU Open FET project, IST 2001-33149 2001-2005, http:\/\/www.dcs.ed.ac.uk\/home\/mrg"},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/3-540-45620-1_5","volume-title":"Automated Deduction - CADE-18","author":"M. Strecker","year":"2002","unstructured":"Strecker, M.: Formal Verification of a Java Compiler in Isabelle. In: Voronkov, A. (ed.) CADE 2002. LNCS, vol.\u00a02392, pp. 63\u201377. Springer, Heidelberg (2002)"},{"key":"15_CR26","unstructured":"Wildmoser, M.: Verified Proof Carrying Code. Ph.D. thesis, Institut f\u00fcr Informatik, Technical University Munchen (2005)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03359-9_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,26]],"date-time":"2023-05-26T11:34:00Z","timestamp":1685100840000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03359-9_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642033582","9783642033599"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03359-9_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}