{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T20:16:24Z","timestamp":1784232984885,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540230175","type":"print"},{"value":"9783540301424","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30142-4_10","type":"book-chapter","created":{"date-parts":[[2010,9,19]],"date-time":"2010-09-19T00:14:09Z","timestamp":1284855249000},"page":"118-135","source":"Crossref","is-referenced-by-count":15,"title":["Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code"],"prefix":"10.1007","author":[{"given":"Nadeem Abdul","family":"Hamid","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Ahmed, A., Appel, A.W., Virga, R.: A stratified semantics of general references embeddable in higher-order logic. In: Proc. 17th Annual IEEE Symposium on Logic in Computer Science, June 2002, pp. 75\u201386 (2002)","DOI":"10.1109\/LICS.2002.1029818"},{"key":"10_CR2","unstructured":"Ahmed, A.J.: Mutable fields in a semantic model of types. In: Talk presented at 2000 PCC Workshop (June 2000)"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Appel, A.W.: Foundational proof-carrying code. In: Proc. 16th Annual IEEE Symposium on Logic in Computer Science, June 2001, pp. 247\u2013258 (2001)","DOI":"10.1109\/LICS.2001.932501"},{"key":"10_CR4","first-page":"243","volume-title":"Proc. 27th ACM Symp. on Principles of Prog. Lang.","author":"A.W. Appel","year":"2000","unstructured":"Appel, A.W., Felty, A.P.: A semantic model of types and machine instructions for proofcarrying code. In: Proc. 27th ACM Symp. on Principles of Prog. Lang., pp. 243\u2013253. ACM Press, New York (2000)"},{"issue":"5","key":"10_CR5","doi-asserted-by":"publisher","first-page":"657","DOI":"10.1145\/504709.504712","volume":"23","author":"A.W. Appel","year":"2001","unstructured":"Appel, A.W., McAllester, D.: An indexed model of recursive types for foundational proofcarrying code. ACM Trans. on Programming Languages and Systems\u00a023(5), 657\u2013683 (2001)","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"10_CR6","first-page":"208","volume-title":"Proc. 2003 ACM Conf. on Prog. Lang. Design and Impl.","author":"J. Chen","year":"2003","unstructured":"Chen, J., Wu, D., Appel, A.W., Fang, H.: A provably sound tal for back-end optimization. In: Proc. 2003 ACM Conf. on Prog. Lang. Design and Impl., pp. 208\u2013219. ACM Press, New York (2003)"},{"key":"10_CR7","first-page":"95","volume-title":"Proc. 2000 ACM Conf. on Prog. Lang. Design and Impl.","author":"C. Colby","year":"2000","unstructured":"Colby, C., Lee, P., Necula, G., Blau, F., Plesko, M., Cline, K.: A certifying compiler for Java. In: Proc. 2000 ACM Conf. on Prog. Lang. Design and Impl., pp. 95\u2013107. ACM Press, New York (2000)"},{"key":"10_CR8","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Coquand, T., Huet, G.: The calculus of constructions. Information and Computation\u00a076, 95\u2013120 (1988)","journal-title":"Information and Computation"},{"key":"10_CR9","first-page":"198","volume-title":"Proc. 30th ACM Symp. on Principles of Prog. Lang.","author":"K. Crary","year":"2003","unstructured":"Crary, K.: Towards a foundational typed assembly language. In: Proc. 30th ACM Symp. on Principles of Prog. Lang., January 2003, pp. 198\u2013212. ACM Press, New York (2003)"},{"key":"10_CR10","unstructured":"Crary, K., Sarkar, S.: A metalogical approach to foundational certified code. Technical Report CMU-CS-03-108, Carnegie Mellon University (January 2003)"},{"key":"10_CR11","unstructured":"Felty, A.: Semantic models of types and machine instructions for proof-carrying code. Talk presented at 2000 PCC Workshop (June 2000)"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Hamid, N.A., Shao, Z.: Coq code for interfacing hoare logic and type systems for fpcc, Available at flint.cs.yale.edu\/flint\/publications (May 2004)","DOI":"10.21236\/ADA436479"},{"key":"10_CR13","unstructured":"Hamid, N.A., Shao, Z., Trifonov, V., Monnier, S., Ni, Z.: A syntactic approach to foundational proof carrying-code. Journal of Automated Reasoning, Special issue on Proof- Carrying Code (to appear)"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Hamid, N.A., Shao, Z., Trifonov, V., Monnier, S., Ni, Z.: A syntactic approach to foundational proof carrying-code. In: Proc. 17th Annual IEEE Symposium on Logic in Computer Science, June 2002, pp. 89\u2013100 (2002)","DOI":"10.1109\/LICS.2002.1029819"},{"key":"10_CR15","first-page":"85","volume-title":"Proc. 25th ACM Symp. on Principles of Prog. Lang.","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. on Principles of Prog. Lang., January 1998, pp. 85\u201397. ACM Press, New York (1998)"},{"key":"10_CR16","first-page":"106","volume-title":"Proc. 24th ACM Symp. on Principles of Prog. Lang.","author":"G. Necula","year":"1997","unstructured":"Necula, G.: Proof-carrying code. In: Proc. 24th ACM Symp. on Principles of Prog. Lang., January 1997, pp. 106\u2013119. ACM Press, New York (1997)"},{"key":"10_CR17","unstructured":"Necula, G.: Compiling with Proofs. PhD thesis, School of Computer Science, Carnegie Mellon Univ. (September 1998)"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Necula, G., Lee, P.: Safe kernel extensions without run-time checking. In: Proc. 2nd USENIX Symp. on Operating System Design and Impl., pp. 229\u2013243 (1996)","DOI":"10.1145\/238721.238781"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Necula, G.C., Schneck, R.R.: A sound framework for untrustred verification-condition generators. In: Proc. 18th Annual IEEE Symposium on Logic in Computer Science, June 2003, pp. 248\u2013260 (2003)","DOI":"10.1109\/LICS.2003.1210065"},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037116","volume-title":"Typed Lambda Calculi and Applications","author":"C. Paulin-Mohring","year":"1993","unstructured":"Paulin-Mohring, C.: Inductive definitions in the system Coq\u2014rules and properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, Springer, Heidelberg (1993)"},{"key":"10_CR21","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"Automated Deduction - CADE-16","author":"F. Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf - a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 202\u2013206. Springer, Heidelberg (1999)"},{"key":"10_CR22","unstructured":"Swadi, K.N., Appel, A.W.: Typed machine language and its semantics, Unpublished manuscript available at www.cs.princeton.edu\/~appel\/papers (July 2001)"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Tan, G., Appel, A.W., Swadi, K.N., Wu, D.: Construction of a semantic model for a typed assembly language. In: 5th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2004) (January 2004) (to appear)","DOI":"10.1007\/978-3-540-24622-0_4"},{"key":"10_CR24","unstructured":"The Coq Development Team. The Coq proof assistant reference manual. The Coq release v7.1 (October 2001)"},{"key":"10_CR25","unstructured":"Werner, B.: Une Th\u00e9orie des Constructions Inductives. PhD thesis, A L\u2019Universit\u00e9 Paris 7, Paris, France (1994)"},{"issue":"1","key":"10_CR26","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"A.K. Wright","year":"1994","unstructured":"Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation\u00a0115(1), 38\u201394 (1994)","journal-title":"Information and Computation"},{"key":"10_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-36575-3_25","volume-title":"Programming Languages and Systems","author":"D. Yu","year":"2003","unstructured":"Yu, D., Hamid, N.A., Shao, Z.: Building certified libraries for PCC: Dynamic storage allocation. In: Degano, P. (ed.) ESOP 2003. LNCS, vol.\u00a02618, pp. 363\u2013379. Springer, Heidelberg (2003)"}],"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_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,25]],"date-time":"2025-02-25T22:37:10Z","timestamp":1740523030000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30142-4_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540230175","9783540301424"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30142-4_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}