Principal typings for Java-like languages.
Elena Zucca
Abstract
The purpose of the talk is twofold. First, we give
a general notion of type system supporting separate compilation and
inter-checking, and a formal definition of soundess and completeness
of inter-checking w.r.t. global compilation. These properties are
important in practice since they allow selective recompilation. In
particular, we show that they are guaranteed when the type system has
principal typings and provides sound and complete entailment relation
between type environments and types. The second contribution is more
specific, and is an instantiation of the notion of type system
previously defined for Featherweight Java [IgarashiEtAl99] with method
overloading and field hiding. The aim is to show that it is possible
to define type systems for Java-like languages, which, differently
from those used by standard compilers, have principal typings, hence
can be used as a basis for selective recompilation