Computing Publications

Publications Home » Towards an Existential Types Mode...

Towards an Existential Types Model for Java Wildcards

Nicholas Cameron, Erik Ernst, Sophia Drossopoulou

Conference or Workshop Paper
Formal Techniques for Java-like Programs (FTfJP) 2007
July, 2007

Wildcards extend Java generics by softening the mismatch between subtype and parametric polymorphism. Although they are a key part of the Java 5.0 programming language, a type system including wildcards has never been proven type sound. Wildcards have previously been formalised as existential types. In this paper we extend FGJ, a featherweight formalisation of Java with generics, with existential types. We prove that this calculus, ExistsJ, is type sound, and illustrate how it models wildcards in the Java Programming Language. ExistsJ is not a full model for Java wildcards, because it does not support lower bounds for wildcards. We discuss why ExistsJ can not be easily extended with lower bounds, and how full Java wildcards could be modelled in a type sound way.

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