A formal type system for Java

Abstract

The primary objective of this paper is threefold: First, we present an evaluation of the state of the art on Java static semantics. Accordingly, we discuss the completeness and the soundness of the most prominent proposals recently advanced in the literature. Moreover, we discuss their compliance with respect to the Java language specification. Second, we report a brief evaluation of the official Java language specification. Third, we show how the definition of a realistic static semantics for full Java could be addressed. We exhibit the technical difficulties and discuss the semantic traits that could be used to address them.