A three-valued type system for true positives detection in Java-like languages

Soundness of type systems is an important property to guarantee the absence of certain kinds of runtime errors, that is, no false negatives can occur. Unfortunately, for well-known theoretical limits, there are many programs that cannot be typed correctly, even though they will never manifest runtime errors, that is, false positives can occur. Minimizing the rate of false positives makes static type analysis more effective, especially for dynamically typed languages. In this paper we propose a new approach to type systems, aiming to distinguish true from potentially false positives, and, thus, to provide useful hints on those lines of code that definitely contain a bug that sooner or later will occur. To this aim, we define a three-valued type system for Featherweight Java which is sound in the usual sense, but can also distinguish true positives from potentially false ones.