{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:21:46Z","timestamp":1751660506080,"version":"3.41.0"},"reference-count":24,"publisher":"Association for Computing Machinery (ACM)","issue":"12","license":[{"start":{"date-parts":[[2012,12,1]],"date-time":"2012-12-01T00:00:00Z","timestamp":1354320000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000144","name":"Division of Computer and Network Systems","doi-asserted-by":"publisher","award":["CCF-0702681CNS-050955"],"award-info":[{"award-number":["CCF-0702681CNS-050955"]}],"id":[{"id":"10.13039\/100000144","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["CCF-0702681CNS-050955"],"award-info":[{"award-number":["CCF-0702681CNS-050955"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Commun. ACM"],"published-print":{"date-parts":[[2012,12]]},"abstract":"<jats:p>We consider the problem of specifying combinations of data structures with complex sharing in a manner that is declarative and results in provably correct code. In our approach, abstract data types are specified using relational algebra and functional dependencies. We describe a language of decompositions that permits the user to specify different concrete representations for relations, and show that operations on concrete representations soundly implement their relational specification. We also describe an auto-tuner that automatically identifies the best decomposition for a particular workload. It is easy to incorporate data representations synthesized by our compiler into existing systems, leading to code that is simpler, correct by construction, and comparable in performance to the code it replaces.<\/jats:p>","DOI":"10.1145\/2380656.2380677","type":"journal-article","created":{"date-parts":[[2012,11,29]],"date-time":"2012-11-29T15:02:27Z","timestamp":1354201347000},"page":"91-99","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["An introduction to data representation synthesis"],"prefix":"10.1145","volume":"55","author":[{"given":"Peter","family":"Hawkins","sequence":"first","affiliation":[{"name":"Stanford University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Rinard","sequence":"additional","affiliation":[{"name":"MIT"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alex","family":"Aiken","sequence":"additional","affiliation":[{"name":"Stanford University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[{"name":"Tel-Aviv University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kathleen","family":"Fisher","sequence":"additional","affiliation":[{"name":"Tufts University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2012,12]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Supercomputing (Nov.","author":"Ahmed N.","year":"2000","unstructured":"Ahmed , N. , Mateev , N. , Pingali , K. , Stodghill , P. A framework for sparse matrix code synthesis from high-level specifications . In Supercomputing (Nov. 2000 ). IEEE Computer Society , 58. Ahmed, N., Mateev, N., Pingali, K., Stodghill, P. A framework for sparse matrix code synthesis from high-level specifications. In Supercomputing (Nov. 2000). IEEE Computer Society, 58."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.846301"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008617930959"},{"key":"e_1_2_1_4_1","series-title":"LNCS","volume-title":"CAV","author":"Berdine J.","year":"2007","unstructured":"Berdine , J. , Calgano , C. , Cook , B. , Distefano , D. , O'Hearn , P.W. , Wies , T. , Yang , H. Shape analysis for composite data structures . In CAV ( 2007 ), volume 4590 of LNCS . Springer , Berlin\/ Heidelberg , 178--192. Berdine, J., Calgano, C., Cook, B., Distefano, D., O'Hearn, P.W., Wies, T., Yang, H. Shape analysis for composite data structures. In CAV (2007), volume 4590 of LNCS. Springer, Berlin\/Heidelberg, 178--192."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11531142_12"},{"key":"e_1_2_1_6_1","volume-title":"VLDB","author":"Chaudhuri S.","year":"1997","unstructured":"Chaudhuri , S. , Narasayya , V.R. An efficient cost-driven index selection tool for Microsoft SQL Server . In VLDB ( 1997 ), Morgan Kaufmann Publishers , San Francisco, CA , 146--155. Chaudhuri, S., Narasayya, V.R. An efficient cost-driven index selection tool for Microsoft SQL Server. In VLDB (1997), Morgan Kaufmann Publishers, San Francisco, CA, 146--155."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/52.210604"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/357062.357064"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449782"},{"key":"e_1_2_1_10_1","volume-title":"International Workshop on Alias Confinement and Ownership (Jul.","author":"F\u00e4hndrich M.","year":"2003","unstructured":"F\u00e4hndrich , M. , Leino , K.R.M. Heap monotonic typestates . In International Workshop on Alias Confinement and Ownership (Jul. 2003 ). F\u00e4hndrich, M., Leino, K.R.M. Heap monotonic typestates. In International Workshop on Alias Confinement and Ownership (Jul. 2003)."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993504"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11319-2_17"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503276"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_28"},{"key":"e_1_2_1_15_1","series-title":"LNCS","volume-title":"CAV","author":"Lee O.","year":"2011","unstructured":"Lee , O. , Yang , H. , Petersen , R. Program analysis for overlaid data structures . In CAV ( 2011 ), volume 6806 of LNCS . Springer , Berlin\/ Heidelberg . 592--608. Lee, O., Yang, H., Petersen, R. Program analysis for overlaid data structures. In CAV (2011), volume 6806 of LNCS. Springer, Berlin\/Heidelberg. 592--608."},{"key":"e_1_2_1_16_1","series-title":"LNCS","volume-title":"Static Analysis","author":"McCloskey B.","year":"2011","unstructured":"McCloskey , B. , Reps , T. , Sagiv , M. Statically inferring complex heap, array, and numeric invariants . In Static Analysis ( 2011 ), volume 6337 of LNCS . Springer , Berlin\/ Heidelberg , 71--99. McCloskey, B., Reps, T., Sagiv, M. Statically inferring complex heap, array, and numeric invariants. In Static Analysis (2011), volume 6337 of LNCS. Springer, Berlin\/Heidelberg, 71--99."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1142473.1142552"},{"key":"e_1_2_1_18_1","volume-title":"LICS","author":"Reynolds J.C.","year":"2002","unstructured":"Reynolds , J.C. Separation logic: A logic for shared mutable data structures . In LICS ( 2002 ), 55--74, invited paper. Reynolds, J.C. Separation logic: A logic for shared mutable data structures. In LICS (2002), 55--74, invited paper."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1244381.1244394"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567771"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542522"},{"key":"e_1_2_1_22_1","volume-title":"Conference on Domain-Specific Languages (DSL '97)","author":"Smaragdakis Y.","year":"1997","unstructured":"Smaragdakis , Y. , Batory , D. Di STi L : a transformation library for data structures . In Conference on Domain-Specific Languages (DSL '97) ( Oct. 1997 ), USENIX, 257--271. Smaragdakis, Y., Batory, D. DiSTiL: a transformation library for data structures. In Conference on Domain-Specific Languages (DSL '97) (Oct. 1997), USENIX, 257--271."},{"key":"e_1_2_1_23_1","series-title":"LNCS","volume-title":"ECOOP","author":"Vaziri M.","year":"2007","unstructured":"Vaziri , M. , Tip , F. , Fink , S. , Dolby , J. Declarative object identity using relation types . In ECOOP ( 2007 ), volume 4609 of LNCS . Springer , Berlin\/ Heidelberg , 54--78. Vaziri, M., Tip, F., Fink, S., Dolby, J. Declarative object identity using relation types. In ECOOP (2007), volume 4609 of LNCS. Springer, Berlin\/Heidelberg, 54--78."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375624"}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2380656.2380677","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2380656.2380677","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:48:13Z","timestamp":1750240093000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2380656.2380677"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,12]]},"references-count":24,"journal-issue":{"issue":"12","published-print":{"date-parts":[[2012,12]]}},"alternative-id":["10.1145\/2380656.2380677"],"URL":"https:\/\/doi.org\/10.1145\/2380656.2380677","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"type":"print","value":"0001-0782"},{"type":"electronic","value":"1557-7317"}],"subject":[],"published":{"date-parts":[[2012,12]]},"assertion":[{"value":"2012-12-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}