Data representation synthesis

9 years 5 months ago
Data representation synthesis
We consider the problem of specifying combinations of data structures with complex sharing in a manner that is both declarative lts 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 permit the user to specify different concrete representations for relations, and show that operations on concrete representations soundly implement their relational specification. 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. Categories and Subject Descriptors D.3.3 [Programming LanLanguage Constructs and Features—Abstract data types, Data types and structures; E.2 [Data Storage Representations] General Terms Languages, Design, Algorithms, Performance, Verification Keywords Synthesis, Composite Data Structures
Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin
Added 17 Sep 2011
Updated 17 Sep 2011
Type Journal
Year 2011
Where PLDI
Authors Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin C. Rinard, Mooly Sagiv
Comments (0)