Principal typings for Java-like languages

The contribution of the paper is twofold. First, we define a general notion of type system equipped with an entailment relation between type environments; this generalisation serves as a pattern for instantiating type systems able to support separate compilation and interchecking of Java-like languages, and allows 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. 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, in contrast to those used by standard compilers, have princip...

• Type: Conference
• Year: 2004
• Where: POPL
• Authors: Davide Ancona, Elena Zucca
• Keywords: Entailment Relation, POPL 2004, Principal Typings, Programming Languages, Selective Recompilation