Principal Typings for Java-Like Languages

Davide Ancona and Elena Zucca

To appear at Principles of Programming Languages (POPL04), Venice, Italy, January 14-16, 2004


The contribution of the paper is twofold. First, we provide 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 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.

Server START Conference Manager
Update Time 19 Sep 2003 at 17:40:43
Start Conference Manager
Conference Systems