{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:56:11Z","timestamp":1725551771487},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540297352"},{"type":"electronic","value":"9783540322474"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11575467_3","type":"book-chapter","created":{"date-parts":[[2005,11,11]],"date-time":"2005-11-11T13:58:51Z","timestamp":1131717531000},"page":"19-36","source":"Crossref","is-referenced-by-count":5,"title":["Data Refinement with Low-Level Pointer Operations"],"prefix":"10.1007","author":[{"given":"Ivana","family":"Mijajlovi\u0107","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hongseok","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1145\/503272.503289","volume-title":"POPL 2002","author":"A. Banerjee","year":"2002","unstructured":"Banerjee, A., Naumann, D.A.: Representation independence, confinement and access control (extended abstract). In: POPL 2002, pp. 166\u2013177. ACM, New York (2002)"},{"key":"3_CR2","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1145\/604131.604156","volume-title":"POPL 2003","author":"C. Boyapati","year":"2003","unstructured":"Boyapati, C., Liskov, B., Shrira, L.: Ownership types for object encapsulation. In: POPL 2003, pp. 213\u2013223. ACM, New York (2003)"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-45337-7_4","volume-title":"ECOOP 2001 - Object-Oriented Programming","author":"D.G. Clarke","year":"2001","unstructured":"Clarke, D.G., Noble, J., Potter, J.M.: Simple ownership types for object containment. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol.\u00a02072, pp. 53\u201376. Springer, Heidelberg (2001)"},{"key":"3_CR4","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511663079","volume-title":"Data Refinement: Model-Oriented Proof Methods and their Comparison","author":"W.-P. Roever de","year":"1998","unstructured":"de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge Tracts in Theoretical Computer Science, vol.\u00a047. Cambridge University Press, Cambridge (1998)"},{"key":"3_CR5","volume-title":"A Discipline of Programming","author":"E. Dijkstra","year":"1976","unstructured":"Dijkstra, E.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/3-540-16442-1_14","volume-title":"ESOP 86","author":"J. He","year":"1986","unstructured":"He, J., Hoare, C.A.R., Sanders, J.W.: Data refinement refined. In: Robinet, B., Wilhelm, R. (eds.) ESOP 1986. LNCS, vol.\u00a0213, pp. 187\u2013196. Springer, Heidelberg (1986)"},{"key":"3_CR7","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"C.A.R. Hoare","year":"1972","unstructured":"Hoare, C.A.R.: Proof of correctness of data representations. Acta Informatica\u00a01, 271\u2013281 (1972)","journal-title":"Acta Informatica"},{"key":"3_CR8","first-page":"271","volume-title":"OOPLA 1991","author":"J. Hogg","year":"1991","unstructured":"Hogg, J.: Islands: Aliasing protection in object-oriented languages. In: OOPLA 1991, pp. 271\u2013285. ACM Press, New York (1991)"},{"issue":"2","key":"3_CR9","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1145\/130943.130947","volume":"3","author":"J. Hogg","year":"1992","unstructured":"Hogg, J., Lea, D., Wills, A., de Champeaux, D., Holt, R.: The geneva convention on the treatment of object aliasing. OOPS Messenger\u00a03(2), 11\u201316 (1992)","journal-title":"OOPS Messenger"},{"key":"3_CR10","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/360204.375719","volume-title":"POPL 2001","author":"S. Istiaq","year":"2001","unstructured":"Istiaq, S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: POPL 2001, pp. 14\u201326. ACM Press, London (2001)"},{"issue":"5","key":"3_CR11","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1145\/570886.570888","volume":"24","author":"K.R.M. Leino","year":"2002","unstructured":"Leino, K.R.M., Nelson, G.: Data abstraction and information hiding. ACM Trans. on Program. Lang. and Syst.\u00a024(5), 491\u2013553 (2002)","journal-title":"ACM Trans. on Program. Lang. and Syst."},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/978-3-540-30538-5_35","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"I. Mijajlovi\u0107","year":"2004","unstructured":"Mijajlovi\u0107, I., Torp-Smith, N., O\u2019Hearn, P.W.: Refinement and separation contexts. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 421\u2013433. Springer, Heidelberg (2004)"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Mijajlovic, I., Yang, H.: Data refinement with low-level pointer operations. Manuscript (2005), Available at http:\/\/ropas.snu.ac.kr\/~hyang\/paper\/full-ps.ps","DOI":"10.1007\/11575467_3"},{"key":"3_CR14","first-page":"313","volume-title":"LICS 2004","author":"D. Naumann","year":"2004","unstructured":"Naumann, D., Barnett, M.: Towards imperative modules: Reasoning about invariants and sharing of mutable state. In: LICS 2004, pp. 313\u2013323. IEEE, Los Alamitos (2004)"},{"key":"3_CR15","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1145\/964001.964024","volume-title":"POPL 2004","author":"P.W. O\u2019Hearn","year":"2004","unstructured":"O\u2019Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: POPL 2004, pp. 268\u2013280. ACM, Venice (2004)"},{"key":"3_CR16","volume-title":"Talk at MFPS 2000","author":"U.S. Reddy","year":"2000","unstructured":"Reddy, U.S.: Talk at MFPS 2000. Hokoken, New Jersey (2000)"},{"issue":"1","key":"3_CR17","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/j.scico.2004.01.007","volume":"50","author":"U.S. Reddy","year":"2004","unstructured":"Reddy, U.S., Yang, H.: Correctness of data representations involving heap data structures. Science of Computer Programming\u00a050(1), 257\u2013305 (2004)","journal-title":"Science of Computer Programming"},{"key":"3_CR18","first-page":"55","volume-title":"LICS 2002, vol. 17","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS 2002, vol. 17, pp. 55\u201374. IEEE, Copenhagen (2002)"},{"issue":"1","key":"3_CR19","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF01806033","volume":"9","author":"I. Stark","year":"1996","unstructured":"Stark, I.: Categorical models for local names. Lisp and Symbolic Comput.\u00a09(1), 77\u2013107 (1996)","journal-title":"Lisp and Symbolic Comput."}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11575467_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:57:30Z","timestamp":1605643050000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11575467_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540297352","9783540322474"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/11575467_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}