Related Works

Relevant

Incrementalization

In general, our incrementalization task is simpler because the unchanged data elements are already abstracted/summarized for us.
DITTO: Automatic Incrementalization of Data Structure Invariant Checks (in Java).
- http://portal.acm.org/citation.cfm?id=1250734.1250770
  - (Done looking through references)
- Given Java objects with recursive "data structure invariant check" functions, they instrument the functions to cache/memoize the return value for the arguments. Any later modifications to the data structure trigger re-execution of not only all the recursive calls containing the dirty arguments but also their parent callers for any calls that have different return values than before -- this could continue recursively until the root node is reached. Like us, they break up each call into a single function body vs. the chain of calls and avoid re-executing entire chains when possible. Unlike us they have to hold every node and its checker args in memory instead of abstracting it; it seems like bitmap graphics compared to our vector graphics.

Hybrid type checking

Hybrid type checking.
- http://portal.acm.org/citation.cfm?id=1111037.1111059
  - (Stuck; don't know what is relevant or not)
  - He defines a variant of lambda calculus with mandatory refinement/set type annotations and a compilation process that sends casts to a theorem prover. If the theorem prover can refute the relation or provide a counterexample, compilation fails. If the prover succeeds, no extra code is inserted. If the prover times out, a dynamic check is inserted.
Dynamic Typing with dependent types.
- They added dependent/set types and simple{} and dependent{} blocks to lambda calculus: "simple" means verify dependent constraints at run-time, and "dependent" means programmer must annotate the code in detail and a type checker will verify them. "Pay as you go" strategy is to add dependent types after you get the code working.
Ccured: Type-safe retrofitting of legacy code.
Dependent types for low-level programming.
- http://portal.acm.org/citation.cfm?id=1762221
- A flow-insensitive and path-insensitive analysis of annotated C programs determines what assertions to add, then later flow-sensitive optimizing/compilation passes remove/prove some of the assertions, especially trivial/redundant ones. The goal is to make pointer arithmetic and union types safer.
  - "Once the program compiles, the programmer typically needs to add or modify annotations in order to eliminate run-time errors that are due to insufficient or incorrect annotations."
  - "Most previous dependent type systems restrict the dependencies such that all assertions fall within theories with simple decision procedures, rejecting programs with assertions that cannot be discharged statically. In Deputy we expect that some assertions will remain in the program even after optimization, either because they use operators for which we do not have efficient decision procedures or because the programmer did not fully specify all the necessary invariants." (emphasis added)

Liquid types

Liquid types
- http://doi.acm.org/10.1145/1375581.1375602
- They take Hindley-Milner type inference on ML and add refinements (predicates). They limit subtyping to certain provable implication checks to preserve decidability. By inferring types they dramatically reduce the annotations needed.
  - "Of course, there may be safe programs which cannot be well- typed in our system due either to an inappropriate choice of qualifiers or the conservativeness of our notion of subtyping. In the former case, we can use the readable results of the inference to manually add more qualifiers, and in the latter case we can use the results of the inference to insert a minimal set of run-time checks [Ou et al. 2004, Flanagan 2006]."
Type-based Data Structure Verification
- http://doi.acm.org/10.1145/1542476.1542510
  - Now their refinement types can capture properties of recursive data structures (i.e. linked lists) like sortedness and uniqueness. They show how guaranteed uniqueness can prove non-aliasing (could it be useful for expressing separating disjunction too?) So they use fold and unfold operations. They can handle many examples including red-black trees.
Low-level Liquid Types
- http://doi.acm.org/10.1145/1706299.1706316
  - They analyze C code by using SSA to separate mutable and immutable memory locations. The type include bounds information. They use "version control" for a metaphor of unfolding and folding, which seems different than our practice of shortening/lengthening a collection when unfold/fold. For function calls they separate the heap into the part that will be modified and the part that won't, inspired by the separation logic frame rule.
  - "...at the lowest levels of the software stack... we cannot fall back on dynamic mechanisms to protect against bugs, crashes, or malicious attacks."
  - "In contrast [to shape analysis], LTLL is an automatic technique that uses a combination of low-level types and predicate abstraction to compute invariants for data stored inside collections without using information about the shape of the underlying structure. In future work we would like to investigate ways to improve the precision of LTLL by enriching it with shape (or reachability) information, which would allow us to determine when a location has been removed from a collection."

Shape analysis

Relational inductive shape analysis.
- http://portal.acm.org/citation.cfm?id=1328438.1328469
- Parts to build on: shape domain parameterized by numeric data constraint domain, coordinating shape and domain for widening, red-black tree example with inverse invariant, order invariant, and balance invariant.
- Possibly relevant: type inference, checker segment regions
- Not relevant: backward unfolding
Shape analysis with structural invariant checkers.
- http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.63.3631
- Maybe don't need to say anything about this paper in the text, since it's subsumed by the POPL 08.
Compositional shape analysis by means of bi-abduction
- http://doi.acm.org/10.1145/1480881.1480917
- Their goal is infer preconditions and postconditions for procedures that are especially precise without having to do whole-program analysis. They use abduction to learn how a procedure's precondition needs additional frames to meet the preconditions of the procedures that it calls, but they also use bi-abduction to infer what spatial predicates are not necessary for the called procedures (anti-frames) and can be dropped.
- Possibly relevant to us: they define a ordering relationship for "quality of solutions," where false is the lowest quality assertion. The ordering is "used to inform design choices," since actually finding the best solution can be expensive.

Data structures

Red-Black Trees in a Functional Setting.
- http://portal.acm.org/citation.cfm?id=968583
- They present a recursive functional algorithm for insertion into a red-black tree using pattern matching for simplicity.

Haven't looked at yet

* List of references in Johnson et al. "A Systematic Incrementalization Technique and its Application to Hardware Design" http://www.cs.indiana.edu/~sjohnson/papers/Johnson-Liu-Zhang-99.pdf

* [11, 22, 17, 38, 6, 45, 50, 31, 29, 30, 34, 28] incrementalization references in Liu et al

* Liu and Teitelbaum "Systematic derivation of incremental programs" (31 in Liu et al), also mentioned in Ditto paper

* Yellin and Strom. INC: A language for incremental computations (50 in Liu et al)

* In DITTO paper: Algorithm incrementalization has been the subject of considerable research [9, 17, 18, 19, 12]; see [21] for a comprehensive bibliography of early work.

* Types and Type Inference sections of POPL '10? http://www.cse.psu.edu/popl/10/program.html

* Design Patterns in Separation Logic http://www.cs.cmu.edu/~neelk/design-patterns-tldi09.pdf

* Static Contract Checking for Haskell? http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-737.pdf

Zee et al says: The goal of shape analysis is typically to ver- ify only data structure shape properties (and not full functional correctness properties such as the change of data structure con- tent)

"Parameterized shape analyses such as TVLA have been extended to prove properties beyond shape, such as ordering of list elements [52] and the correctness of a binary search tree with a set interface [68] (using manually devised and un- verified rules for updating instrumentation predicates).

Not particularly relevant

Incrementalization Across Object Abstraction.
- http://portal.acm.org/citation.cfm?id=1094811.1094848
- Given a program that calls query/read and update/write methods on an object, they automatically compute a new program that rewrites repeated expensive queries as simpler queries of sets that are kept current by changes to the update methods. Unlike us, they work with unordered lists (sets). Like us, they rewrite O(N^2) programs as O(N).
INC: a language for incremental computation.
- http://portal.acm.org/citation.cfm?id=103135.103137
- INC is a functional language to manipulate multisets/bags. It has Apply/Filter/Reduce etc. but not recursion or the least fixed point operator. Under the hood, intermediate results are saved. Changes to sets are also saved as sets of inserts, deletes, and remains. You call a function with a set as an argument, but internally it only runs the function for set members that are new or deleted, then merges the changes into the previous results. What interests me is the idea of compositional change propagation.
Self-Adjusting Computation.
Contracts Made Manifest.
- Too theoretical about latent vs. manifest contracts.
- Findler and Felleisen 2002
- not helpful since we're only concerned about typing data, not functions
- Threesomes, With and Without Blame
  - Jeremy G. Siek (University of Colorado at Boulder), Philip Wadler (University of Edinburgh)
- not helpful since we're only concerned about typing data, not functions
- From Contracts Made Manifest paper:
  - - "By contrast, manifest contracts are integrated into the type system, which tracks, for each value, the most recently checked contract. Hybrid types [Flanagan 2006] are a well-known example in this style; others include the work of Ou et al. [2004], Wadler and Findler [2009], and Gronski et al. [2006]."
- Integrating Typed and Untyped Code in a Scripting Language.
  - Tobias Wrigstad (Purdue University), Francesco Zappa Nardelli (INRIA), Sylvain Lebresne (Purdue University), Johan Ostlund (Purdue University), Jan Vitek (Purdue University)
- types seem limited to just object-oriented classes, not arbitrary boolean predicates

Page updated

Google Sites

Report abuse