Dulma Rodriguez, Type inference for RAJA - a static heap space analysis of OO-programs.
Type inference for RAJA - a static heap space analysis of OO-programs.
RAJA is a type system for a compile-time analysis of heap-space requirements for Java style object-oriented programs. The system was first described in ESOP 2006 by Hofmann and Jost, where the soundness of the analysis has been proven. Later, in CSL 2009, Hofmann and Rodriguez described efficient type checking for an annotated version of the system. Our next goal is to infer the typing annotations automatically in order to make the system feasible for programming.
In this talk we will present a type inference algorithm consisting of two main parts:
- A sound and complete constraint-generation system.
- An algorithm for solving the subtyping constraints by eliminating view variables which is inspired by the Fourier-Motzkin algorithm for eliminating variables from a system of linear inequalities.