Definite Reference Mutability
Reference immutability type systems such as Javari and ReIm ensure that a given reference cannot be used to mutate the referenced object. These systems are conservative in the sense that a mutable references may not be truly mutable, but mutable due to approximation.
In this paper, we present ReM (for definite Re[ference] M[utability]). It separates potentially mutable references into (1) definitely mutable, and (2) maybe mutable, i.e., references whose mutability is due to inherent approximation. In addition, we propose a CFL-reachability system for reference immutability, and prove that it is equivalent to ReIm/ReM, thus building a novel framework for reasoning about correctness of reference immutability type systems. We have implemented ReM and applied it on a large benchmark suite. Our results show that approximately 86.5% of all potentially mutable references are definitely mutable.
Sat 21 Jul
|11:00 - 11:25|
|11:25 - 11:50|
|11:50 - 12:15|
Ana MilanovaRensselaer Polytechnic InstituteDOI
|12:15 - 12:40|
Neville GrechUniversity of Athens, George KastrinisUniversity of Athens, Yannis SmaragdakisUniversity of AthensDOI