Università di Torino

Research on "Formal Methods in Computing"

Even More Principal Typings for Java-like Languages

Davide ANCONA, Ferruccio DAMIANI , Sophia DROSSOPOULOU , and Elena ZUCCA

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.


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
year      = {2004}

["Formal Methods in Computing" group] [Department's HOME]

Last update: Jun 12, 2006