This file is not kept current. See my web page for more up-to-date information. The url is: http://theory.stanford.edu/~kfisher. Last modified: Oct. 22, 1997 Contents of directory: +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ tapos98.ps Title: On the relationship between classes, objects and data abstraction Authors: K. Fisher and J.C. Mitchell Pub: TAPOS, to appear Note: An earlier version of this paper appeared in Marktoberdorf Proceedings, Springer LNCS, 1996. Abstract: While most object-oriented programming is done in class-based languages, the trend in theoretical study has been to develop formal systems that are object-based, without classes and often without explicit inheritance mechanisms. This paper studies the correspondence between class constructs of the form found in \CC{}, Eiffel, and Java and object primitives of the form used in recent type-theoretic studies. One insight is that classes require both an extensible aggregate, to serve as the basis for inheritance, and a non-extensible form of object to support subtyping; typed object calculi without extensible objects or extensible records do not seem adequate for conventional class-based programming. We develop our analysis by comparing three approaches to class-based programming, the first using records of object components called ``premethods'' and the latter two using an extensible form of object called a ``prototype.'' While the first approach is simplest, using fewer primitive operations on objects, it does not seem to accurately provide several features of conventional class-based languages. In the latter two approaches, we give more comprehensive treatments of classes by combining prototypes with standard abstraction mechanisms. All three treatments of classes are based on typed translations into provably sound object calculi. +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ marktoberdorf.ps Title: On the relationship between classes, objects and data abstraction Authors: K. Fisher and J.C. Mitchell Pub: Marktoberdorf Proceedings, Springer LNCS, 1996, to appear. Abstract: While most object-oriented programming is done in class-based languages, the trend in theoretical study has been to develop formal systems that are object-based, without classes and often without explicit inheritance mechanisms. This paper studies the correspondence between object primitives and class constructs of the form found in C++, Eiffel, and Java. The main qualitative insight is that such classes require both an extensible aggregate, to serve as the basis for inheritance, and a non-extensible form of object to support subtyping. We compare three approaches to modeling classes, the first using records of object components called ``premethods'' and the latter two using an extensible form of object called a ``prototype.'' While the first approach uses fewer primitive operations on objects, it does not provide several important features of class-based languages. In the latter two approaches, we overcome these deficiencies by combining prototypes with standard abstraction mechanisms. All three treatments of classes use translations into provably sound object calculi. +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ fmoods.ps Title: Analysis for Concurrent Objects Authors: P. DiBlasio, K. Fisher, and C. Talcott Pub: FMOODS '97 Abstract: We present a set-based control flow analysis for an imperative, concurrent object calculus extending the Fisher-Honsell-Mitchell functional object-oriented calculus described in~\cite{fisherhm}. The analysis is shown to be sound with respect to a transition-system semantics. +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ concur96.{ps,dvi} Title: A Calculus for Concurrent Objects Authors: P. DiBlasio and K. Fisher Pub: Concur '96 Abstract: This paper presents an imperative and concurrent extension of the functional object-oriented calculus described in \cite{FisherHM}. It belongs to the family of so-called prototype-based object-oriented languages, in which objects are created from existing ones via the inheritance primitives of object extension and method override. Concurrency is introduced through the identification of objects and processes. To our knowledge, the resulting calculus is the first concurrent object calculus to be studied. We define an operational semantics for the calculus via a transition relation between configurations, which represent snapshots of the run-time system. Our static analysis includes a type inference system, which statically detects {\it message-not-understood} errors, and an effect system, which guarantees that synchronization code, specified via guards, is side-effect free. We present a subject reduction theorem, modified to account for imperative and concurrent features, and type and effect soundness theorems. +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ imptypes.{ps,dvi} Title: Classes = Objects + Data Abstraction Authors: K. Fisher and J.C. Mitchell Pub: Stanford Technical Note: STAN-CS-TN-96-31 Abstract: We describe a type-theoretic foundation for object systems that include ``interface types'' and ``implementation types,'' in the process accounting for access controls such as \CC{} {\tt private, protected} and {\tt public} levels of visibility. Our approach begins with a basic object calculus that provides a notion of object, method lookup, and object extension (an object-based form of inheritance). In this calculus, the type of an object gives an interface, as a set of methods (public member functions) and their types, but does not imply any implementation properties such as the presence or layout of any hidden internal data. We extend the core object calculus with a higher-order form of data abstraction mechanism that allows us to declare supertypes of an abstract type and a list of methods guaranteed not to be present. This results in a flexible framework for studying and improving practical programming languages where the type of an object gives certain implementation guarantees, such as would be needed to statically determine the offset of a function in a method lookup table or safely implement binary operations without exposing the internal representation of objects. We prove type soundness for the entire language using operational semantics and an analysis of typing derivations. Two insights that are immediate consequences of our analysis are the identification of an anomaly associated with \CC{} {\tt private virtual} functions and a principled, type-theoretic explanation (for the first time, as far as we know) of the link between subtyping and inheritance in \CC{}, Eiffel and related languages. +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ fct-95.{ps,dvi} Title: A Delegation-based Object Calculus with Subtyping Authors: K. Fisher and J.C. Mitchell Pub: Fundamentals of Computation Theory (FCT'95), Springer LNCS 965, 1995, 42-61. Abstract: This paper presents an untyped object calculus that reflects the capabilities of so-called delegation-based object-oriented languages. A type inference system allows static detection of errors, such as {\it message not understood,} while at the same time allowing the type of an inherited method to be specialized to the type of the inheriting object. The main advance over previous work is the provision for subtyping in the presence of delegation primatives. This is achieved by distinguishing a prototype, whose methods may be extended or replaced, from an object, which only responds to messages for which it already has methods. An advantage of this approach is that we have full subtyping without restricting the ``run-time'' use of inheritance. Type soundness is proved using operational semantics and an analysis of typing derivations. +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ objects-njc.{dvi,ps} Title: A Lambda Calculus of Objects and Method Specialization Authors: K. Fisher and J.C. Mitchell Pub: Nordic J. Computing, 1:3-37, 1994. Preliminary version appeared in Proc. IEEE Symp. on Logic in Computer Science, 1993, 26-38. (objects-lics93.dvi.Z) Abstract: This paper presents an untyped lambda calculus, extended with object primitives that reflect the capabilities of so-called delegation-based object-oriented languages. A type inference system allows static detection of errors, such as {\it message not understood,} while at the same time allowing the type of an inherited method to be specialized to the type of the inheriting object. Type soundness is proved using operational semantics and examples illustrating the expressiveness of the pure calculus are presented. +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ tapos.{dvi,ps} Title: The Development of Type Systems for Object-Oriented Languages Authors: K. Fisher and J.C. Mitchell Pub: To appear in the TAPOS Special Issue on Types. This paper is an updated version of "Notes on Typed Object-Oriented Programming," which appeared in Proc. Theoretical Aspects of Computer Software, Springer LNCS 789, 1994, 844-885. This paper also appears as Stanford Technical Note STAN-CS-TN-96-30 Abstract: This paper, which is partly tutorial in nature, summarizes some basic research goals in the study and development of typed object-oriented programming languages. These include both immediate repairs to problems with existing languages and the long-term development of more flexible and expressive, yet type-safe, approaches to program organization and design. The technical part of the paper is a summary and comparison of three object models from the literature. We conclude by discussing approaches to selected research problems, including changes in the type of a method from super class to sub class and the use of types that give information about the implementations as well as the interfaces of objects. Such implementation types seem essential for adequate typing of binary operations on objects, for example. +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ whatis-oop.{dvi,ps} Title: Whatis an Object-Oriented Programming Language Authors: K. Fisher and J.C. Mitchell Abstract: This document is a set of rough notes on basic features of object-oriented programming. It is based on the first section of the paper ``Notes on typed object-oriented programming,'' {\it Proc. Theoretical Aspects of Computer Software,} Springer LNCS 789, 1994, pages 844--885.