Computing Publications

Publications Home » Even More Principal Typings for J...

Even More Principal Typings for Java-like Languages

Davide Ancona, Ferruccio Damiani, Sophia Drossopoulou, Elena Zucca

Conference or Workshop Paper
ECOOP Workshop on Formal Techniques for Java Programs (FTfJP 2004)
June, 2004

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 system 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.

Flexible, source level dynamic linking and re-linking

Java Semantics
Language Design
PDF of full publication (208 kilobytes)
(need help viewing PDF files?)
BibTEX file for the publication
Conditions for downloading publications from this site. built & maintained by Ashok Argent-Katwala.