Research on "Formal Methods in Computing"

Even More Principal Typings for Java-like Languages

Work partially supported by IST-2001-33477 DART, and APPSEM II - Thematic network IST-2001-38957.

ABSTRACT. We propose a new type system for Java-like languages which allows compilation of a class in isolation, that is, in a context where no information is available on other classes. Indeed, by this type system it is possible to infer the assumptions guaranteeing type correctness of a class c, and generate (abstract) bytecode for c, by just inspecting the source code of c. Then, a collection of classes can be safely linked together without further inspection of the classes' code, provided that each class has been typechecked in isolation (intra-checking), and that the mutual class assumptions are satisfied (inter-checking). In other words, the type s ystems supports compositional analysis, as formally guaranteed by the fact that it has principal typings. We also develop an algorithm for inter-checking, and prove it correct.

• pdf

BIBTEX.

@inproceedings{tipoW-ADDZ:FTfJP-04,
author    = {D. Ancona and F. Damiani and S. Drossopoulou and E. Zucca},
title     = {Even More Principal Typings for Java-like Languages},
booktitle = {Electronic proceedings of FTfJP'04
             (http://www.cs.ru.nl/ftfjp/)},
year      = {2004}
}