A core calculus for Java exceptions

In this paper we present a simple calculus (called CJE) in order to fully i nvestigate the exception mechanism of Java, and in particular its interacti on with inheritance, which turns out to be non trivial. Moreover, we show t hat the type system for the calculus directly driven by the Java Language S pecification (called FULL) uses too many types, in the sense that there are different types which provide exactly the same information. Hence, we obta in from FULL a simplified type system called MIN where equivalent types hav e been identified. We show that this is useful both for type-checking optim ization and for clarifying the static semantics of the language. The two ty pe systems axe proved to satisfy the subject reduction property.