Title: Modular Inference for Array Checks Optimization

Abstract:
  An array check can be safely eliminated if it is valid under the
context in which it is invoked.  In this paper, we propose a modular
inference mechanism that is based on an advanced form of typing,
called sized type.  We apply this to a core imperative language to
discover program contexts for which array checks may be safely
eliminated.  Our inference is modular as it is able to process each
method independently, and yet exploit the different contexts of its
multiple callers.  We achieve this by turning each partially-safe
check into a precondition that is propagated up its callers' contexts
for further analysis.  This approach provides for a highly accurate
interprocedural optimization.  The results of our modular inference
can be used to guide a range of program specializations that trade-off
code space for more aggressive optimization.  We have implemented a
prototype inference system and have also proven its soundness.
Initial experiments suggest that such an inference system is viable.