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

Keywords
SLURP
Java Semantics
Language Design
PDF of full publication (208 kilobytes)
(need help viewing PDF files?)
BibTEX file for the publication
N.B.
Conditions for downloading publications from this site.
 

pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.