{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:04:18Z","timestamp":1725566658833},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540255963"},{"type":"electronic","value":"9783540320333"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-32033-3_29","type":"book-chapter","created":{"date-parts":[[2010,9,28]],"date-time":"2010-09-28T00:20:02Z","timestamp":1285633202000},"page":"394-406","source":"Crossref","is-referenced-by-count":1,"title":["A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code"],"prefix":"10.1007","author":[{"given":"Amy P.","family":"Felty","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"29_CR1","doi-asserted-by":"crossref","unstructured":"Ahmed, A.J., Appel, A.W., Virga, R.: A stratified semantics of general references embeddable in higher-order logic. In: Seventeenth Annual IEEE Symposium on Logic in Computer Science, July 2002, pp. 75\u201386 (2002)","DOI":"10.1109\/LICS.2002.1029818"},{"key":"29_CR2","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, pp. 243\u2013253 (2000)","DOI":"10.1145\/325694.325727"},{"issue":"5","key":"29_CR3","doi-asserted-by":"publisher","first-page":"657","DOI":"10.1145\/504709.504712","volume":"13","author":"A.W. Appel","year":"2001","unstructured":"Appel, A.W., McAllester, D.: An indexed model of recursive types for foundational proof-carrying code. ACM Transactions on Programming Languages and Systems\u00a013(5), 657\u2013683 (2001)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"29_CR4","doi-asserted-by":"crossref","unstructured":"Chang, B.-Y.E., Chlipala, A., Necula, G.C., Schneck, R.R.: The open verifier framework for foundational verifiers. In: ACM SIGPLAN Workshop on Types in Language Design and Implementation (January 2005)","DOI":"10.1145\/1040294.1040295"},{"key":"29_CR5","unstructured":"Coq Development Team. The Coq Proof Assistant reference manual: Version 7.4. Technical report, INRIA (2003)"},{"key":"29_CR6","doi-asserted-by":"crossref","unstructured":"Crary, K., Sarkar, S.: Toward a foundational typed assembly language. In: Thirtieth ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 198\u2013212 (2003)","DOI":"10.1145\/604131.604149"},{"key":"29_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-540-30142-4_10","volume-title":"Theorem Proving in Higher Order Logics","author":"N.A. Hamid","year":"2004","unstructured":"Hamid, N.A., Shao, Z.: Interfacing hoare logic and type systems for foundational proof-carrying code. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 118\u2013135. Springer, Heidelberg (2004)"},{"issue":"3-4","key":"29_CR8","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1023\/B:JARS.0000021012.97318.e9","volume":"31","author":"N.A. Hamid","year":"2003","unstructured":"Hamid, N.A., Shao, Z., Trifonov, V., Monnier, S., Ni, Z.: A syntactic approach to foundational proof-carrying code (extended version). Journal of Automated Reasoning\u00a031(3-4), 191\u2013229 (2003)","journal-title":"Journal of Automated Reasoning"},{"key":"29_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1007\/10721959_2","volume-title":"Seventeenth International Conference on Automated Deduction","author":"N.G. Michael","year":"2000","unstructured":"Michael, N.G., Appel, A.W.: Machine instruction syntax and semantics in higher order logic. In: Seventeenth International Conference on Automated Deduction, June 2000. LNCS, pp. 7\u201324. Springer, Heidelberg (2000)"},{"issue":"3","key":"29_CR10","doi-asserted-by":"publisher","first-page":"528","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), 528\u2013569 (1999)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"29_CR11","volume-title":"Fifth International Conference and Symposium on Logic Programming","author":"G. Nadathur","year":"1988","unstructured":"Nadathur, G., Miller, D.: An overview of \u03bbProlog. In: Bowen, K., Kowalski, R. (eds.) Fifth International Conference and Symposium on Logic Programming, MIT Press, Cambridge (1988)"},{"key":"29_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/3-540-48660-7_25","volume-title":"Automated Deduction - CADE-16","author":"G. Nadathur","year":"1999","unstructured":"Nadathur, G., Mitchell, D.J.: System description: Teyjus \u2014 a compiler and abstract machine based implementation of \u03bbProlog. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 287\u2013291. Springer, Heidelberg (1999)"},{"key":"29_CR13","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1145\/263699.263712","volume-title":"24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"G. Necula","year":"1997","unstructured":"Necula, G.: Proof-carrying code. In: 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 1997, pp. 106\u2013119. ACM Press, New York (1997)"},{"key":"29_CR14","unstructured":"Swadi, K.N., Appel, A.W.: Foundational semantics for TAL syntactic rules via typed machine language (March 2002), \n                  \n                    http:\/\/www.cs.princeton.edu\/kswadi\/papers\/tml.ps"},{"key":"29_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-540-24622-0_4","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"G. Tan","year":"2004","unstructured":"Tan, G., Appel, A.W., Swadi, K.N., Wu, D.: Construction of a semantic model for a typed assembly language. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 30\u201343. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Term Rewriting and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-32033-3_29.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T03:45:35Z","timestamp":1620013535000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32033-3_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540255963","9783540320333"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32033-3_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}