Two papers on static type systems for objects
Two papers on the foundations of static type systems for object-
oriented programming languages are now available for anonymous FTP.
The first is an expanded version of our POPL paper "Object-Oriented
Programming without Recursive Types." The second describes an
extension to support "friendly functions" like those of C++ in typed
models of objects based on bounded quantification.
Both papers develop their results, in detail, as programs in the typed
lambda-calculus F-omega-sub, but both (especially the first) are
intended to be accessible to the general reader. Source code (in
Standard ML) and a sun4 binary for a prototype f-omega-sub compiler
are also available, along with a set of tutorial exercises covering
the material presented in the first paper.
FTP instructions follow the abstracts.
Benjamin C. Pierce
David N. Turner
Simple Type-Theoretic Foundations
For Object-Oriented Programming
Benjamin C. Pierce and David N. Turner
We develop a formal, type-theoretic account of the basic mechanisms of
object-oriented programming: encapsulation, message passing,
subtyping, and inheritance. The main technical achievement is a
substantial simplification in the underlying typed lambda-calculus in
which our account is presented, which we obtain by modeling object
encapsulation in terms of existential types rather than the recursive
records used in recent studies by Cardelli, Bruce, and Mitchell.
Statically Typed Friendly Functions
via Partially Abstract Types
Benjamin C. Pierce David N. Turner
A well-known shortcoming of the object model of Simula and Smalltalk
is the inability to deal cleanly with methods that require access to
the internal state of more than one object at a time. Recent language
designs have therefore extended the basic object model with notions
such as "friends' methods" and "protected features," which allow
external access to the internal state of objects but limit the scope
in which such access can be used. We show that a variant of this idea
can be added to any type-theoretic model of the basic object-oriented
mechanisms (encapsulation, message passing, and inheritance), using a
construction based on Cardelli and Wegner's partially abstract types,
a refinement of Mitchell and Plotkin's type-theoretic treatment of
To retrieve the files, proceed as follows. Remember to set the
connection type to binary; otherwise compressed files will come out as
garbage on the other end!
ftp ftp.dcs.ed.ac.uk [or 220.127.116.11]
password: <your mail address>
binary [don't forget this!]