Computing Publications

Publications Home » A Model for Java Wildcards

A Model for Java Wildcards

Nicholas Cameron, Sophia Drossopoulou, Erik Ernst

Conference or Workshop Paper
ECOOP 08
Eurepean Conference for Object-Oriented Programming
Lecture Notes in Computer Science
July, 2008
Springer-Verlag, LNCS
Abstract

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.

Keywords
Java Semantics
Language Design
SLURP
PDF of full publication (278 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.