{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T14:27:00Z","timestamp":1725460020210},"publisher-location":"Boston","reference-count":19,"publisher":"Kluwer Academic Publishers","isbn-type":[{"type":"print","value":"1402081405"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/1-4020-8141-3_27","type":"book-chapter","created":{"date-parts":[[2006,2,21]],"date-time":"2006-02-21T15:15:11Z","timestamp":1140534911000},"page":"333-347","source":"Crossref","is-referenced-by-count":6,"title":["Prototyping Proof Carrying Code"],"prefix":"10.1007","author":[{"given":"Martin","family":"Wildmoser","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tobias","family":"Nipkow","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerwin","family":"Klein","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sebastian","family":"Nanz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"Appel, A. W. (2001). Foundational proof-carrying code. In 16th Annual IEEE Symposium on Logic in Computer Science (LICS\u2019 01), pages 247\u2013258.","DOI":"10.1109\/LICS.2001.932501"},{"key":"27_CR2","doi-asserted-by":"crossref","unstructured":"Appel, A. W. and Felty, A. P. (2000). A semantic model of types and machine instructions for proof-carrying code. In 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u2019 00), pages 243\u2013253.","DOI":"10.1145\/325694.325727"},{"key":"27_CR3","unstructured":"Aspinall, D., Beringer, L., Hofmann, M., Loidl, H.W. (2003) A Resource-aware Program Logic for a JVM-like Language In Trends in Functional Programming, editor: S. Gilmore, Edinburgh"},{"key":"27_CR4","doi-asserted-by":"crossref","unstructured":"Berghofer, S. and Nipkow, T. (2000). Proof terms for simply typed higher order logic. In Theorem Proving in Higher Order Logics, Springer LNCS vol. 1869, editors: J. Harrison, M. Aagaard","DOI":"10.1007\/3-540-44659-1_3"},{"key":"27_CR5","doi-asserted-by":"crossref","unstructured":"Berghofer (2003). Program Extraction in simply-typed Higher Order Logic. In Types for Proofs and Programs, International Workshop, (TYPES 2002), Springer LNCS, editors: H. Geuvers, F. Wiedijk","DOI":"10.1007\/3-540-39185-1_2"},{"key":"27_CR6","doi-asserted-by":"crossref","unstructured":"Colby, C., Lee, P., Necula, G. C., Blau, F., Plesko, M., and Cline, K. (2000). A certifying compiler for Java. In Proc. ACM SIGPLAN conf. Programming Language Design and Implementation, pages 95\u2013107.","DOI":"10.1145\/349299.349315"},{"key":"27_CR7","doi-asserted-by":"crossref","unstructured":"Hamid, N., Shao, Z., Trifonov, V., Monnier, S., and Ni, Z. (2002). A syntactic approach to foundational proof-carrying code. In Proc. 17th IEEE Symp. Logic in Computer Science, pages 89\u2013100.","DOI":"10.1109\/LICS.2002.1029819"},{"key":"27_CR8","unstructured":"Klein, G. (2003). Verified Java Bytecode Verification. PhD thesis, Institut fur Informatik, Technische Universit\u00e4t M\u00fcnchen."},{"key":"27_CR9","unstructured":"League, C., Shao, Z., and Trifonov, V. (2002). Precision in practice: A type-preserving Java compiler. Technical Report YALEU\/DCS\/TR-1223, Department of Computer Science, Yale University."},{"key":"27_CR10","doi-asserted-by":"crossref","unstructured":"Morrisett, G., Walker, D., Crary, K., and Glew, N. (1998). From system F to typed assembly language. In Proc. 25th ACM Symp. Principles of Programming Languages, pages 85\u201397. ACM Press.","DOI":"10.1145\/268946.268954"},{"key":"27_CR11","doi-asserted-by":"crossref","unstructured":"Necula, G. C. (1997). Proof-carrying code. In Proc. 24th ACM Symp. Principles of Programming Languages, pages 106\u2013119. ACM Press.","DOI":"10.1145\/263699.263712"},{"key":"27_CR12","unstructured":"Necula, G. C. (1998). Compiling with Proofs. PhD thesis, Carnegie Mellon University."},{"key":"27_CR13","doi-asserted-by":"crossref","unstructured":"Necula, G. C. and Lee, P. (2000). Proof generation in the touchstone theorem prover. In McAllester, D., editor, Automated Deduction \u2014 CADE-17, volume 1831 of Lect. Notes in Comp. Sci., pages 25\u201344. Springer-Verlag.","DOI":"10.1007\/10721959_3"},{"key":"27_CR14","unstructured":"Necula, G. C. and Schneck, R. R. (2002). A gradual approach to a more trustworthy, yet scalable, proof-carrying code. In Voronkov, A., editor, Proc.CADE-18, 18th International Conference on Automated Deduction, Copenhagen, Denmark, volume 2392 of Lect. Notes in Comp. Sci., pages 47\u201362. Springer-Verlag."},{"key":"27_CR15","unstructured":"Necula, G. C. and Schneck, R. R. (2003). A sound framework for untrustred verification-condition generators. In Proc. IEEE Symposium on Logic in Computer Science. (LICS03), pages 248\u2013260."},{"key":"27_CR16","unstructured":"Nipkow, T., Paulson, L. C., and Wenzel, M. (2002). Isabelle\/HOL-A Proof Assistant for Higher-Order Logic, volume 2283 of Lect. Notes in Comp. Sci. Springer."},{"key":"27_CR17","series-title":"Technical Report","volume-title":"A Machine-Checked Model for a Java-Like Language, Virtual Machine and Compiler","author":"G. Klein","year":"2004","unstructured":"Klein, G. and Nipkow, T. (2004) A Machine-Checked Model for a Java-Like Language, Virtual Machine and Compiler Technical Report, National ICT Australia, Sydney"},{"key":"27_CR18","doi-asserted-by":"crossref","unstructured":"Wildmoser, M. and Nipkow, T. (2004) Certifying machine code safety: shallow versus deep embedding. TPHOLs 2004","DOI":"10.1007\/978-3-540-30142-4_22"},{"key":"27_CR19","unstructured":"VeryPCC website in Munich (2004), \n                    http:\/\/isabelle.in.tum.de\/verypcc\/\n                    \n                  ."}],"container-title":["IFIP International Federation for Information Processing","Exploring New Frontiers of Theoretical Informatics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/1-4020-8141-3_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T20:28:14Z","timestamp":1619555294000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/1-4020-8141-3_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["1402081405"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/1-4020-8141-3_27","relation":{},"subject":[]}}