[Prev][Next][Index][Thread]
OOL design and semantics papers
The following papers on the design, type-checking, and semantics of a
functional, statically-typed, object-oriented language, TOOPLE, are now
available for anonymous ftp:
1. Safe Type Checking in a Statically-Typed Object-Oriented Programming Language
by Kim B. Bruce. To Appear in Proc ACM Symp. Principles of Programming
Languages, 1993.
2. An operational semantics for TOOPLE: A statically-typed object-oriented
programming language, by Kim B. Bruce, Jonathan Crabtree, and Gerald Kanapathy.
3. Type checking in TOOPLE is decidable, by Kim B. Bruce, Jon Crabtree,
Allyn Dimock, Robert Muller, Thomas P. Murtagh, Robert van Gent.
They may be obtained by anonymous ftp from bull.cs.williams.edu, (for those
whose name servers have difficulty finding the machine, its numeric
address is 137.165.5.2).
Login as anonymous and type your id as password when requested. To get to
the proper directory, type:
cd pub/kim
To receive the papers, type
get TCPOPL.dvi
get TPLNatSem.dvi
get TpCkAlgo.dvi
The second and third papers are preliminary versions for conference submission,
so I would be grateful for any comments or suggestions for clarification on
them. Full versions will be available later.
The README file in the same directory contains descriptions of other
papers on object-oriented languages and their semantics which can also be found
in the same directory.
The abstracts of the three papers follow:
---------------------
Safe Type Checking in a Statically-Typed Object-Oriented Programming Language
by Kim B. Bruce. To Appear in Proc ACM Symp. Principles of Programming
Languages, 1993.
10/92
ABSTRACT
In this paper we introduce a statically-typed, functional, object-oriented
programming language, TOOPL, which supports classes, objects, methods, instance
variables, subtypes, and inheritance.
It has proved to be surprisingly difficult to design statically-typed
object-oriented languages which are nearly as expressive as SmallTalk and
yet have no holes in their typing systems. A particular problem with statically
type checking object-oriented languages is determining
whether a method provided in a superclass will continue to type check
when inherited in a subclass. This problem is solved in our
language by providing type checking rules which guarantee that a method
which type checks as part of a class will type check correctly in all legal
subclasses in which it is inherited. This feature enables
library providers to provide only the interfaces of classes with executables
and still allow users to safely create subclasses.
The design of TOOPL has been guided by an analysis of the semantics
of the language, which is given in terms of a sufficiently rich model of
the F-bounded second-order lambda calculus. This semantics supported
the language design by provided a means of proving that the type-checking rules
for the language are sound, ensuring that well-typed terms
produce objects of the appropriate type. In particular, in a well-typed program
it is impossible to send a message to an object which lacks a
corresponding method.
-----------------
An operational semantics for TOOPLE: A statically-typed object-oriented
programming language, by Kim B. Bruce, Jonathan Crabtree, and Gerald Kanapathy.
Preliminary Conference Submission 11/92
ABSTRACT
In this paper we present an operational semantics for the language
TOOPLE, a statically-typed, functional, object-oriented programming language
which has a number of desirable properties.
The operational semantics, given in the form of a natural semantics, is
significantly simpler than the previous denotational semantics for the language.
A ``subject reduction'' theorem for the natural semantics provides a proof
that the language is type-safe. We also show that the natural semantics is
consistent with the denotational semantics of the language.
----------------
Type checking in TOOPLE is decidable, by Kim B. Bruce, Jon Crabtree, Allyn
Dimock, Robert Muller, Thomas P. Murtagh, Robert van Gent.
Preliminary Conference Submission 12/92
ABSTRACT
Over the last several years, much interesting work has been done in modelling
object-oriented programming languages in terms of extensions of the bounded
second-order lambda calculus, $F_{\le}$. Unfortunately, it has recently been
shown by Pierce (\cite{Pierce92}) that type checking
$F_{\le}$ is undecidable. Moreover he showed that the undecidability arises in
the seemingly simpler problem of determining whether one type is a subtype of
another.
In \cite{Bruce92,BrPOPL93}, the first author introduced a statically-typed,
functional, object-oriented programming language, TOOPL, which supports classes,
objects, methods, instance variables, subtypes, and inheritance. The semantics
of TOOPL is based on $F_{\le}$, so the question arises whether type checking in
this language is decidable.
In this paper we show that type checking for TOOPLE, a minor variant of TOOPL
(Typed Object-Oriented Programming Language),
is decidable. The proof proceeds by showing that subtyping is
decidable, that all terms of TOOPLE have minimum types (which are in fact
computable), and then using these two results to show that type checking
is decidable. Interestingly, conditional statements introduce significant
problems which necessitated the computation of generalized least upper bounds
of types. The interaction of the least upper bounds with the implicit
recursion in object and class definitions and the contravariant nature
of function spaces makes the computation of appropriate least upper bounds
more subtle than might be expected. Our algorithm fails to be polynomial in the
size of the term because the size of the type of a term can be exponential
in the size of the term. Nevertheless, it performs well in practice.
This paper concentrates on the language without instance variables, though
the results can be extended to the full language, at the cost of some added
complexity.
-----------------
Kim Bruce, Williams College
kim@cs.williams.edu