{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,24]],"date-time":"2025-09-24T09:29:35Z","timestamp":1758706175470},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540230175"},{"type":"electronic","value":"9783540301424"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30142-4_22","type":"book-chapter","created":{"date-parts":[[2010,9,18]],"date-time":"2010-09-18T20:14:09Z","timestamp":1284840849000},"page":"305-320","source":"Crossref","is-referenced-by-count":38,"title":["Certifying Machine Code Safety: Shallow Versus Deep Embedding"],"prefix":"10.1007","author":[{"given":"Martin","family":"Wildmoser","sequence":"first","affiliation":[]},{"given":"Tobias","family":"Nipkow","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","unstructured":"VeryPCC project, http:\/\/isabelle.in.tum.de\/verypcc\/ (2003)"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"Appel, A.W.: Foundational proof-carrying code. In: 16th Annual IEEE Symposium on Logic in Computer Science (LICS 2001), June 2001, pp. 247\u2013258 (2001)","DOI":"10.1109\/LICS.2001.932501"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"Appel, A.W., Felty, A.P.: A semantic model of types and machine instructions for proof-carrying code. In: 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2000), January 2000, pp. 243\u2013253 (2000)","DOI":"10.1145\/325694.325727"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/3-540-39185-1_2","volume-title":"Types for Proofs and Programs","author":"S. Berghofer","year":"2003","unstructured":"Berghofer, S.: Program extraction in simply-typed higher order logic. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol.\u00a02646, pp. 21\u201338. Springer, Heidelberg (2003)"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-45842-5_2","volume-title":"Types for Proofs and Programs","author":"S. Berghofer","year":"2002","unstructured":"Berghofer, S., Nipkow, T.: Executing higher order logic. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol.\u00a02277, p. 24. Springer, Heidelberg (2002)"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/3-540-44659-1_3","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Berghofer","year":"2000","unstructured":"Berghofer, S., Nipkow, T.: Proof terms for simply typed higher order logic. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, pp. 38\u201352. Springer, Heidelberg (2000)"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"Chen, J., Wu, D., Appel, A.W., Fang, H.: A provably sound tal for back-end optimization. In: Programming Languages Design and Implementation (PLDI), ACM Sigplan (2003)","DOI":"10.1145\/781131.781155"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Colby, C., Lee, P., Necula, G.C., Blau, F., Plesko, M., Cline, K.: A certifying compiler for Java. In: Proc. ACM SIGPLAN conf. Programming Language Design and Implementation, pp. 95\u2013107 (2000)","DOI":"10.1145\/349299.349315"},{"key":"22_CR9","unstructured":"Gerwin, K., Tobias, N.: A machine-checked model for a Java-like language, virtual machine and compiler. Research report, National ICT Australia, Sydney (2004)"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Hamid, N., Shao, Z., Trifonov, V., Monnier, S., Ni, Z.: A syntactic approach to foundational proof-carrying code. In: Proc. 17th IEEE Symp. Logic in Computer Science, July 2002, pp. 89\u2013100 (2002)","DOI":"10.1109\/LICS.2002.1029819"},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Homeier, P.V., Martin, D.F.: Secure mechanical verification of mutually recursive procedures, pp. 1\u201319 (2003)","DOI":"10.1016\/S0890-5401(03)00133-0"},{"key":"22_CR12","unstructured":"Klein, G.: Verified Java Bytecode Verification. PhD thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (2003)"},{"key":"22_CR13","first-page":"85","volume-title":"Proc. 25th ACM Symp. Principles of Programming Languages","author":"G. Morrisett","year":"1998","unstructured":"Morrisett, G., Walker, D., Crary, K., Glew, N.: From system F to typed assembly language. In: Proc. 25th ACM Symp. Principles of Programming Languages, pp. 85\u201397. ACM Press, New York (1998)"},{"key":"22_CR14","first-page":"106","volume-title":"Proc. 24th ACM Symp. Principles of Programming Languages","author":"G.C. Necula","year":"1997","unstructured":"Necula, G.C.: Proof-carrying code. In: Proc. 24th ACM Symp. Principles of Programming Languages, pp. 106\u2013119. ACM Press, New York (1997)"},{"key":"22_CR15","unstructured":"Necula, G.C.: Compiling with Proofs. PhD thesis, Carnegie Mellon University (1998)"},{"key":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"22_CR17","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The Formal Semantics of Programming Languages","author":"G. Winskel","year":"1993","unstructured":"Winskel, G.: The Formal Semantics of Programming Languages. MIT Press, Cambridge (1993)"}],"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-540-30142-4_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,2]],"date-time":"2021-05-02T23:52:18Z","timestamp":1619999538000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30142-4_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540230175","9783540301424"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30142-4_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}