Two papers on static type systems for objects

Two papers on static type systems for objects

Post by David N. Turn » Fri, 23 Apr 1993 00:01:10

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.  Sources (in Standard
ML) and sun4 binaries 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
abstract types.

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                [or]
    login: anonymous
    password: <your mail address>
    cd pub/bcp
    binary                              [don't forget this!]
    get oop.dvi
    get friendly.dvi