Data representation synthesis

We consider the problem of specifying combinations of data structures with complex sharing in a manner that is both 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 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.

• Publication year

  2011

• Venue

  ACM-SIGPLAN Symposium on Programming Language Design and Implementation

• Publication date

  2011-06-01

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/1993498.1993504
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Program Analysis for Overlaid Data Structures

  2011cited by this paper
• Data Structure Fusion

  2010cited by this paper
• Statically Inferring Complex Heap, Array, and Numeric Invariants

  2010cited by this paper
• Shape Analysis of Low-Level C with Overlapping Structures

  2010cited by this paper
• Chameleon: adaptive selection of collections

  2009cited by this paper
• Effective interactive proofs for higher-order imperative programs

  2009cited by this paper
• An integrated proof language for imperative programs

  2009cited by this paper
• Pig latin: a not-so-foreign language for data processing

  2008cited by this paper
• Modular Verification with Shared Abstractions

  2008cited by this paper
• jStar: towards practical verification for java

  2008cited by this paper
• Full functional verification of linked data structures

  2008cited by this paper
• Efficient implementation of tuple pattern based retrieval

  2007cited by this paper
• Declarative Object Identity Using Relation Types

  2007cited by this paper
• LINQ: reconciling object, relations and XML in the .NET framework

  2006cited by this paper
• First-Class Relationships in an Object-Oriented Language

  2005cited by this paper
• Generalized Typestate Checking for Data Structure Consistency

  2005cited by this paper
• Heap Monotonic Typestate

  2003cited by this paper
• Separation logic: a logic for shared mutable data structures

  2002cited by this paper
• Role analysis

  2002cited by this paper
• A Framework for Sparse Matrix Code Synthesis from High-level Specifications

  2000cited by this paper
• An Efficient Cost-Driven Index Selection Tool for Microsoft SQL Server

  1997cited by this paper
• A Relational Approach to the Compilation of Sparse Matrix Programs

  1997cited by this paper
• DiSTiL: A Transformation Library for Data Structures

  1997cited by this paper
• Graph types

  1993cited by this paper
• Automating relational operations on data structures

  1993cited by this paper
• Look ma, no hashing, and no arrays neither

  1991cited by this paper
• Mechanical Translation of Set Theoretic Problem Specifications into Efficient RAM Code-A Case Study

  1987influential reference
• Automatic data structure selection in SETL

  1979cited by this paper
• Programming by Refinement, as Exemplified by the SETL Representation Sublanguage

  1979cited by this paper
• Ieee Transactions on Software Engineering 1 Modular Pluggable Analyses for Data Structure Consistency

  year unknowncited by this paper
• To appear in: CAV 2007. Shape Analysis for Composite Data Structures

  year unknowncited by this paper

• Automatic Data Enumeration for Fast Collections

  2026cites this paper
• Repr Types: One Abstraction to Rule Them All

  2024cites this paper
• Semantic Code Refactoring for Abstract Data Types

  2024influential citation
• COMORP: Rapid prototyping for mathematical database cost models development

  2022cites this paper
• Complexity-guided container replacement synthesis

  2022cites this paper
• Synthesis-powered optimization of smart contracts via data type refactoring

  2022cites this paper
• Compilation of dynamic sparse tensor algebra

  2022cites this paper
• PROGRAMSYNTHESIS FOR SCIENTIFIC COMPUTING

  2021cites this paper
• Report of the Workshop on Program Synthesis for Scientific Computing

  2021cites this paper
• Synthesizing data structure refinements from integrity constraints

  2021cites this paper
• Towards secure IoT programming in Haskell

  2020cites this paper
• Learning quantitative representation synthesis

  2020influential citation
• Learning Data Structure Alchemy

  2019cites this paper
• Design Continuums and the Path Toward Self-Designing Key-Value Stores that Know and Learn

  2019cites this paper
• Deductive optimization of relational data storage

  2019influential citation
• Learning Key-Value Store Design

  2019cites this paper
• Synthesizing database programs for schema refactoring

  2019cites this paper
• The Internals of the Data Calculator

  2018cites this paper
• The Data Calculator: Data Structure Design and Cost Synthesis from First Principles and Learned Cost Models

  2018cites this paper
• Generalized Data Structure Synthesis

  2018influential citation
• The Periodic Table of Data Structures

  2018cites this paper
• C♭: a new modular approach to implementing efficient and tunable collections

  2018cites this paper
• Enforcing Abstract Immutability

  2018cites this paper
• Automated Synthesis of Secure Platform Mappings

  2017cites this paper
• Natural synthesis of provably-correct data-structure manipulations

  2017cites this paper
• Synthesis of Property-Preserving Platform Mappings

  2017cites this paper
• Program synthesis for interactive-security systems

  2017cites this paper
• The End of History? Using a Proof Assistant to Replace Language Design with Library Design

  2017cites this paper
• Synthesis of Property-Preserving Mappings

  2017cites this paper
• A Preliminary Performance Model for Optimizing Software Packet Processing Pipelines

  2017cites this paper
• Seam: provably safe local edits on graphs

  2017cites this paper
• Formal Aspects of Computing Formal Aspects of Computing A fully verified container library

  2017cites this paper
• FSE : G : Cozy : Synthesizing Collection Data Structures

  2017cites this paper
• Using Coq to write fast and correct Haskell

  2017cites this paper
• Data structure synthesis

  2016cites this paper
• Transforming spreadsheet data types using examples

  2016cites this paper
• Fast synthesis of fast collections

  2016cites this paper
• Compilation Using Correct-by-Construction Program Synthesis

  2016cites this paper
• Cozy: synthesizing collection data structures

  2016cites this paper
• Towards a software product line of trie-based collections

  2016cites this paper
• Formal Verification of a Component Platform

  2016cites this paper
• Advancing declarative programming

  2015cites this paper
• Autotuning algorithmic choice for input sensitivity

  2015cites this paper
• Code Generation for Abstract Data Types Based on Program Analysis

  2015influential citation
• An interactive SQL relational interface for querying main-memory data structures

  2015cites this paper
• Profile-guided meta-programming

  2015cites this paper
• Ebb: A DSL for Physical Simluation on CPUs and GPUs

  2015cites this paper
• Code Generation for Abstract Data Types Based on Program Analysis

  2015influential citation
• Developing a dynamic feedback application using JavaScript : responsive feedback evaluation

  2015cites this paper
• Derivable Partial Locking for Algebraic Data Types

  2015cites this paper
• Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant

  2015cites this paper
• A fully verified container library

  2015cites this paper
• Extensible Data-Representation Selection for Correct-by-Construction Program Derivation

  2015cites this paper
• Correct-by-Construction Program Derivation from Specifications to Assembly Language

  2014cites this paper
• Legion: programming distributed heterogeneous architectures with logical regions

  2014cites this paper
• Accessible programming using program synthesis

  2014cites this paper
• Structure Slicing: Extending Logical Regions with Fields

  2014cites this paper
• Dynamic and Interactive Synthesis of Code Snippets

  2014cites this paper
• αRby - An Embedding of Alloy in Ruby

  2014cites this paper
• Auto-parallelization of data structure operations for GPUs

  2014cites this paper
• CodeHint: dynamic and interactive synthesis of code snippets

  2014cites this paper
• A Complete Bibliography of The Bell System Technical Journal , 1960 – 1969

  2013cites this paper
• Compositional Invariant Checking for Overlaid and Nested Linked Lists

  2013cites this paper
• Development of automatically verifiable systems using data representation synthesis

  2013cites this paper
• Algorithmic program synthesis: introduction

  2013cites this paper
• Turning nondeterminism into parallelism

  2013cites this paper
• Parallel schedule synthesis for attribute grammars

  2013cites this paper
• CoCo: Sound and Adaptive Replacement of Java Collections

  2013cites this paper
• An SQL interface for querying a program’s objects

  2013influential citation
• Parallel Layout Engines: Synthesis and Optimization of Tree Traversals

  2013cites this paper
• Inductive representation, proofs and refinement of pointer structures

  2013cites this paper
• Writing data-centric concurrent programs in imperative languages

  2012cites this paper
• Synthesizing iterators from abstraction functions

  2012cites this paper
• K 3 : Language Design for Building Multi-Platform , Domain-Specific Runtimes

  2012cites this paper
• Automated feedback generation for introductory programming assignments

  2012cites this paper
• An introduction to data representation synthesis

  2012influential citation
• Concurrent data representation synthesis

  2012cites this paper
• Automated Semantic Grading of Programs

  2012cites this paper
• Reasoning about Lock Placements

  2012influential citation
• Verification of semantic commutativity conditions and inverse operations on linked data structures

  2011cites this paper
• FTL : Synthesizing a Parallel Layout Engine

  2011cites this paper
• Synthesizing Concurrent Graph Data Structures: A Case Study

  2011cites this paper
• Synthesizing data structure manipulations from storyboards

  2011cites this paper
• Synthesizing data-structure manipulations from storyboards Citation

  2011cites this paper