{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,26]],"date-time":"2026-03-26T09:22:11Z","timestamp":1774516931752,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540243625","type":"print"},{"value":"9783540305576","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-30557-6_8","type":"book-chapter","created":{"date-parts":[[2010,7,2]],"date-time":"2010-07-02T17:53:17Z","timestamp":1278093197000},"page":"83-97","source":"Crossref","is-referenced-by-count":37,"title":["Safe Programming with Pointers Through Stateful Views"],"prefix":"10.1007","author":[{"given":"Dengping","family":"Zhu","sequence":"first","affiliation":[]},{"given":"Hongwei","family":"Xi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"#cr-split#-8_CR1.1","doi-asserted-by":"crossref","unstructured":"Apt, K.R., Olderog, E.-R.: Verification of Sequential and Concurrent Programs, xvi+441 pp. Springer, New York (1991);","DOI":"10.1007\/978-1-4757-4376-0"},{"key":"#cr-split#-8_CR1.2","unstructured":"ISBN 0-387-97532-2 (New York) 3-540- 97532-2 (Berlin)"},{"key":"8_CR2","unstructured":"Constable, R.L., et al.: Implementing Mathematics with the NuPrl Proof Development System, x+299 pp. Prentice-Hall, Englewood Cliffs (1986) ISBN 0-13- 451832-2"},{"key":"8_CR3","unstructured":"Detlefs, D.: An overview of the extended static checking system. In: Workshop on Formal Methods in Software Practice (1996)"},{"key":"8_CR4","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Fahndrich, M., Deline, R.: Adoption and Focus: Practical Linear Types for Imperative Programming. In: Proceedings of the ACM Conference on Programming Language Design and Implementation, Berlin, June 2002, pp. 13\u201324 (2002)","DOI":"10.1145\/512529.512532"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Foster, J., Terauchi, T., Aiken, A.: Flow-sensitive Type Qualifiers. In: ACM Conference on Programming Language Design and Implementation, Berlin, June 2002, pp. 1\u201312 (2002)","DOI":"10.1145\/512529.512531"},{"issue":"1","key":"8_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"Girard, J.-Y.: Linear logic. Theoretical Computer Science\u00a050(1), 1\u2013101 (1987)","journal-title":"Theoretical Computer Science"},{"issue":"10","key":"8_CR8","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM\u00a012(10), 576\u2013580, 583 (1969)","journal-title":"Communications of the ACM"},{"key":"8_CR9","unstructured":"Jim, T., Morrisett, G., Grossman, D., Hicks, M., Baudet, M., Harris, M., Wang, Y.: Cyclone, a Safe Dialect of C (2001), http:\/\/www.cs.cornell.edu\/Projects\/cyclone\/ , Available at http:\/\/www.cs.cornell.edu\/Projects\/cyclone\/"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Mandelbaum, Y., Walker, D., Harper, R.: An effective theory of type refinements. In: Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, Uppsala, Sweden, September 2003, pp. 213\u2013226 (2003)","DOI":"10.1145\/944705.944725"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Necula, G.C., McPeak, S., Weimer, W.: CCured: Type-Safe Retrofitting of Legacy Code. In: Proceedings of the 29th ACM Symposium on Principles of Programming Languages, London, January 2002, pp. 128\u2013139 (2002)","DOI":"10.1145\/503272.503286"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/3-540-36532-X_9","volume-title":"Software Security \u2013 Theories and Systems","author":"Y. Oiwa","year":"2003","unstructured":"Oiwa, Y., Sekiguchi, T., Sumii, E., Yonezawa, A.: Fail-safe ansi-c compiler: An approach to making c programs secure (progress report). In: Okada, M., Pierce, B.C., Scedrov, A., Tokuda, H., Yonezawa, A. (eds.) ISSS 2002. LNCS, vol.\u00a02609, pp. 133\u2013153. Springer, Heidelberg (2003)"},{"key":"8_CR13","unstructured":"Reynolds, J.: Separation Logic: a logic for shared mutable data structures. In: Proceedings of 17th IEEE Symposium on Logic in Computer Science, LICS 2002 (2002), citeseer.nj.nec.com\/reynolds02separation.html"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Xi, H., Chen, C., Chen, G.: Guarded Recursive Datatype Constructors. In: Proceedings of the 30th ACM SIGPLAN Symposium on Principles of Programming Languages, New Orleans, LA, January 2003, pp. 224\u2013235 (2003)","DOI":"10.1145\/604131.604150"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Xi, H., Harper, R.: A Dependently Typed Assembly Language. In: Proceedings of International Conference on Functional Programming, September 2001, pp. 169\u2013180 (2001)","DOI":"10.1145\/507635.507657"},{"key":"8_CR16","unstructured":"Xi, H.: Dependent Types in Practical Programming. PhD thesis, pp. viii+181\u2013viii+189. Carnegie Mellon University (1998), Available at http:\/\/www.cs.cmu.edu\/~hwxi\/DML\/thesis.ps"},{"key":"8_CR17","unstructured":"Xi, H.: Imperative Programming with Dependent Types. In: Proceedings of 15th IEEE Symposium on Logic in Computer Science, Santo Barbara, CA, June 2000, pp. 375\u2013387 (2000)"},{"key":"8_CR18","unstructured":"Xi, H.: Applied Type System (July 2003), Available at http:\/\/www.cs.bu.edu\/~hwxi\/ATS"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/978-3-540-24849-1_25","volume-title":"Types for Proofs and Programs","author":"H. Xi","year":"2004","unstructured":"Xi, H.: Applied Type System (extended abstract). In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085, pp. 394\u2013408. Springer, Heidelberg (2004)"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Xi, H., Pfenning, F.: Dependent Types in Practical Programming. In: Proceedings of 26th ACM SIGPLAN Symposium on Principles of Programming Languages, San Antonio, Texas, January 1999, pp. 214\u2013227 (1999)","DOI":"10.1145\/292540.292560"}],"container-title":["Lecture Notes in Computer Science","Practical Aspects of Declarative Languages"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30557-6_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:22:17Z","timestamp":1605759737000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30557-6_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540243625","9783540305576"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30557-6_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}