Sciweavers

Share
ECOOP
2008
Springer

A Model for Java with Wildcards

8 years 9 months ago
A Model for Java with Wildcards
Wildcards are a complex and subtle part of the Java type system, present since version 5.0. Although there have been various formalisations and partial type soundness results concerning wildcards, to the best of our knowledge, no system that includes all the key aspects of Java wildcards has been proven type sound. This paper establishes that Java wildcards are type sound. We describe a new formal model based on explicit existential types whose pack and unpack operations are handled implicitly, and prove it type sound. Moreover, we specify a translation from a subset of Java to our formal model, and discuss how several interesting aspects of the Java type system are handled.
Nicholas R. Cameron, Sophia Drossopoulou, Erik Ern
Added 19 Oct 2010
Updated 19 Oct 2010
Type Conference
Year 2008
Where ECOOP
Authors Nicholas R. Cameron, Sophia Drossopoulou, Erik Ernst
Comments (0)
books