This file contains titles and abstracts of papers which can be found in ".dvi" and ".ps" form in this directory. They are broken into Research and Teaching and are listed in each category with the most recent first. All papers are available for anonymous ftp from ftp.cs.williams.edu in directory pub/kim. Most of the papers available on this site were developed with the support of a series of NSF Research and Educational grants.
Theses of my most recent honors students are also available on-line.
Slides from some recent public lectures that I have given are also available.
Papers are available in the general categories of Research and Teaching / Education.
Detailed abstracts of all papers follow the listings for TEACHING / EDUCATION.
Abstract LOOJ is an extension of Java obtained by adding bounded parametric polymorphism and new type expressions ThisClass and ThisType, which are similar to MyType in LOOM. Through examples we demonstrate the utility of this language even over very expressive extensions such as GJ. The LOOJ compiler generates standard JVML code and supports instanceof and casts for all types including type variables and the other new type expressions. The core of the LOOJ type system is sound, as demonstrated by a soundness proof for an extension of Featherweight GJ. This paper also highlights difficulties that arise from the use of both classes and interfaces as types in Java.
Abstract In this paper we discuss some of the remaining problems in the design of static type systems for object-oriented programming languages. We look at typing problems involved in writing a simple interpreter as a good example of a simple problem leading to difficult typing issues. The difficulties encountered seem to arise in situations where a programmer desires to simultaneously refine mutually interdependent classes and object types.
Abstract The virtual class construct was first introduced in the language Beta to provide added expressiveness when used with inheritance. Unfortunately, the virtual class construct in Beta is not statically type-safe. In this paper we show how a generalization of the semantics of object-oriented languages with a MyType construct leads to a variant of virtual classes which needs no run-time checks. This results in an object-oriented language in which both parametric types and virtual classes (or types) are well-integrated, and which is statically type-safe.
Keywords: Language design, semantics, virtual classes, parametric polymorphism, static type checking
Abstract Pure object-oriented languages have tended to assume that classes can take the place of modules in programming in the large. We argue that modules are still needed in these languages and present the design of a module construct for our language LOOM which works well with the object-oriented paradigm. We discuss and illustrate the advantages of these modules over a class-only approach. In particular we illustrate the advantages of modules in supporting better control over information hiding, including the support of access like C++'s friends.
Keywords: Language design, modules.
Abstract Parametric types and virtual types have recently been proposed as extensions to Java to support genericity. In this paper we investigate the strengths and weaknesses of each. We suggest a variant of virtual types which has similar expressiveness, but supports safe static type checking. This results in a language in which both parametric types and virtual types are well-integrated, and which is statically type-safe.
Keywords: Language design, virtual types, parametric polymorphism, static type checking
Abstract This paper proposes some relatively minor additions to Java's syntax and semantics in order to increase the expressiveness of the language with little cost in semantic complexity. No changes are suggested that would invalidate or change the semantics of programs written in the current version of Java.
While the main point of the language extensions are to support parametric polymorphism, we also added features which provide better support for binary methods, a kind of method that is often difficult to support in a statically typed language. (See \cite{BinMeth} for an extensive discussion of the difficulties of statically type-checking binary methods.)
Briefly, the changes proposed are to add a ``ThisType' construct to represent the type of ``this'' (the name of the object executing a method), to provide a mechanism for the programmer to specify that a variable hold values of exactly the type given (and not a type that extends it), to reinterpret ``extends'' as ``matching'' rather than ``subtyping'', and to add a form of constrained polymorphism which depends on matching.
Category: Language design
Abstract Virtual classes, which were first used in Beta \cite{VirtClass}, have recently been suggested by Thorup \cite{Thorup} as an extension to Java to support genericity. While virtual classes are a convenient mechanism to support simultaneous modification of mutually recursive classes, they rely on dynamic type checking for type safety. We suggest a variant which has similar expressiveness as virtual classes, but supports safe static type checking. To ease the comparison with earlier work we express our construct as an addition to Java, though similar constructs may be added to a variety of object-oriented languages. For example, this proposal can also be seen as a statically type-safe alternative to Eiffel's ``anchored types''.
Category: Language design
ABSTRACT
Recent years have seen the development of several foundational
models for statically typed object-oriented programming. But despite
their intuitive similarity, differences in the technical machinery
used to formulate the various proposals have made them difficult to
compare.
Using the typed lambda-calculus \FOMEGASUB{} as a common basis, we now offer a detailed comparison of four models: (1) a recursive-record encoding similar to the ones used by Cardelli \cite{Cardelli88}, Reddy \cite{Reddy88->KaminReddy94,KaminReddy94}, Cook \cite{Cook89,CookCH90}, and others; (2) Hofmann, Pierce, and Turner's existential encoding \cite{PTSimple,HofmannPierce94}; (3) Bruce's model based on existential and recursive types \cite{Bruce92}; and (4) Abadi, Cardelli, and Viswanathan's type-theoretic encoding \cite{AbCardV} of a calculus of primitive objects.
Categories: Semantics, Foundations of object-oriented languages.
ABSTRACT
We present the design and rationale of a new
statically-typed object-oriented language, LOOM. LOOM retains most
of the features of the earlier language PolyTOIL. However the
subtyping relation is dropped from LOOM in favor of the matching
relation. ``Hash types'', which are defined in terms of matching,
are introduced to provide some of the benefits of subtyping.
These types can be used to provide support for heterogeneous
data stuctures in LOOM. LOOM is considerably simpler than PolyTOIL, yet
the language is just as expressive. The type system for the language
is decidable and provably type safe. The addition of modules to the
language provides better control over information hiding and allows
the provision of access like that of C++'s friends.
Categories: Type systems and language design for object-oriented languages.
ABSTRACT
While simple static-typing disciplines exist for object-oriented
languages like C++, Object Pascal, and Modula-3, they are often so
restrictive that programmers are forced
to by-pass the type system with type casts. Other languages allow more
freedom, but require run-time checking to pick up the type errors that
their more permissive systems missed.
This paper consists of a survey of problems (illustrated by a series of sample programs) with existing type systems, and suggests ways of improving the expressibility of these systems while retaining static type safety. In particular we will discuss the motivations behind introducing "MyType", "matching", and "bounded matching" into these type systems.
We also suggest a way of simplifying the resulting type system by replacing subtyping by a type system with a new type construct based on matching. Both systems provide support for binary methods, which are often difficult to support in statically-typed languages.
The intent is to avoid pages of type-checking rules and formal proofs, but instead explain why the problems are interesting via the series of sample programs. The technical details (including proofs of subject reduction and type safety) are available elsewhere.
Categories: Type systems for object-oriented languages.
ABSTRACT
In this paper we present the design of PolyTOIL, a provably type-safe
polymorphic object-oriented programming language. PolyTOIL is designed
to be significantly more expressive than statically-typed languages like C++.
Innovative features include
Categories: Type systems, design and semantics of object-oriented languages.
ABSTRACT
Giving types to binary methods causes significant problems for
object-oriented language designers and programmers. This paper offers
a comprehensive description of the problems arising from typing binary
methods, and collects and contrasts diverse views and solutions.
It summarizes the current debate on the problem of binary
methods for a wide audience.
ABSTRACT
In \cite{BrPOPL93}, the first author introduced the language
TOOPLE, a statically-typed functional object-oriented programming language
which has a number of desirable properties. In this and a series of other
papers (\cite{Bruce92,BCDMMG,BrCrKan}), the denotational and natural
semantics of TOOPLE have been presented and shown to be relatively consistent,
subject-reduction and type-safety have been proven,
and the type-checking problem has been shown to be decidable.
In this paper we introduce TOIL, a statically-typed object-oriented imperative language, which is based on the same semantic principles as TOOPLE and shares many of the same desirable properties. We include type-checking rules, an operational semantics, and prove a subject-reduction theorem for TOIL, showing that the operational semantics is type-safe.
This paper is an application of the theoretical work on the semantics of object-oriented programming languages done over the last decade to the design of real object-oriented programming languages.
ABSTRACT
In order to illuminate the fundamental concepts involved in object-oriented
programming languages, we describe the design of TOOPL, a paradigmatic
statically-typed functional object-oriented programming language
which supports classes, objects, methods, hidden instance variables,
subtypes, and inheritance.
It has proven to be quite difficult to design such a language which does not contain holes in the type system. A particular problem with statically type checking object-oriented languages is designing type-checking rules which ensure that methods provided in a superclass will continue to be type correct when inherited in a subclass. The type checking rules for TOOPL have this feature, enabling library suppliers to provide only the interfaces of classes with actual executable code, while still allowing 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 model of the F-bounded second-order lambda calculus with fixed points at both the element and type level. This semantics supported the language design by providing a means to prove that the type checking rules are sound, providing a guarantee that the language is type-safe.
While the semantics of our language is rather complex, involving fixed points at both the element and type level, we believe that this reflects the inherent complexity of the basic features of object-oriented programming languages. Particularly complex features include the implicit recursion inherent in the use of the keyword, self, to refer to the current object, and its corresponding type, MyType. The notions of subclass and inheritance introduce the greatest semantic complexities, whereas the notion of subtype seems relatively straightforward.
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.
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.
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.
ABSTRACT
We relate standard techniques for solving recursive domain
equations to previous models with types interpreted as partial
equivalence relations (per's) over a $D_\infty$ lambda model.
This motivates a particular choice of type functions,
which leads to an extension of such models to higher-order polymorphism.
The resulting models provide natural interpretations for
function spaces, records, recursively defined types, higher-order type
functions, and bounded polymorphic types forall X <: Y. A where the bound
may be of a higher kind. In particular, we may combine recursion
and polymorphism in a way that allows the bound Y in forall X <: Y. A
to be recursively defined. The model may also be used to interpret so-called
F-bounded polymorphism. Together, these features allow us to represent
several forms of type and type functions that seem to
arise naturally in typed object-oriented programming.
ABSTRACT
A simple language is presented which supports inheritance in
object-oriented languages. Using this language, the definitions for
the semantics of inheritance given in \cite{CookCH90} and \cite{MitchPOPL90}
are compared and shown to be equivalent. The equivalence is shown
by presenting and comparing two denotational semantics of the simple
language which capture the essence of each of the earlier semantics.
ABSTRACT
It is unfortunate that in most computing curricula, the uses of
theory and formalisms are limited to the algorithms and theory of computation
courses. In fact, as indicated in the ``Logic in Computer
Science'' panel BKLV98 in SIGCSE `97, logic and logic-related
formalisms can play important parts of a wide variety of courses.
In this paper we explain how logic-based ideas involving formal
operational semantics and
type-checking rules can play an important role in upper-level
principles of programming languages courses.
ABSTRACT
In 1988 the ACM and the IEEE Computer Society formed a Joint Curriculum Task
Force to create a new model curriculum to replace Curriculum '88. Three
years later the committee produced the report, titled Computing Curricula' 91.
In this paper we discuss informally some of the considerations involved
in creating the curriculum report, with the hopes that this will be helpful
to anyone interested in implementing a curriculum in Computer Science based
on the Task Force's report.