A Nominal Theory of Objects with Dependent Types

Martin Odersky, Vincent Cremet, Christine Röckl, Matthias Zenger,
EPFL Lausanne

Proc. ECOOP 03, July 2003

Abstract

We design and study nuObj, a calculus and dependent type system for objects and classes which can have types as members. Type members can be aliases, abstract types, or new types. The type system can model the essential concepts of Java's inner classes as well as virtual types and family polymorphism found in BETA or gbeta. It can also model most concepts of SML-style module systems, including sharing constraints and higher-order functors, but excluding applicative functors. The type system can thus be used as a basis for unifying concepts that so far existed in parallel in advanced object systems and in module systems. The paper presents results on confluence of the calculus, soundness of the type system, and undecidability of type checking.

Paper

in .pdf or .ps or .ps.gz or .dvi .dvi.gz

BibTeX Entry

@InProceedings{odersky-et-al:ecoop03,
  author = 	 {Martin Odersky and Vincent Cremet and Christine R\"ockl and Matthias Zenger},
  title = 	 {A Nominal Theory of Objects with Dependent Types},
  booktitle =	 {Proc. ECOOP'03},
  year =	 2003,
  month =	 july,
  series =	 {Springer LNCS}
}

A Nominal Theory of Objects with Dependent Types

Abstract

Paper

BibTeX Entry

See also