D. Ancona, F. Damiani, S. Drossopoulou, and E. Zucca
Even more principal typings for Java-like
languages
In ECOOP Workshop on Formal Techniques for Java Programs (FTfJP
2004), Oslo, Norway, June 2004
We propose an innovative type system for Java-like
languages which can infer the minimal set of
assumptions guaranteeing type correctness of a class
c, and generate (abstract) bytecode for
c, by inspecting the source code of
c in isolation. We prove the above
properties of our type system by showing that it has
principal typings. As well known, principal typings
support compositional analysis, whereby 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). We also
develop an algorithm for inter-checking, and prove
it correct.
[ bib |
.html |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43