Abstracts

Abstract: The past five years have seen an explosion of foundational models for statically typed object-oriented programming. Many have been presented as translations from high-level object notations to typed lambda-calculi with subtyping, differing in technical details but sharing underlying intuitions. This tutorial develops a uniform notational framework -- a typed lambda-calculus with subtyping, higher-order polymorphism, existential types, and recursive types -- and uses it to compare and contrast four previously studied models.
[Joint work with Kim Bruce and Luca Cardelli.]

Abstract:: Component override is a powerful and common technique in object oriented programming; strongly typed systems need to impose restrictions on the types of the components involved. Usually, the type of the overriding component must be a subtype of the overridden component. For methods, this results into the sound contravariant rule, which requires the argument types of the overriding method to be supertypes of the argument types of the overridden method. For ST&T, a type system for Smalltalk we adopted a 'permissive' approach, which allows covariant override for instance variables and any override for method. All subclasses are treated as subtypes, and message expressions are type checked by considering the types of methods in the receiver and all its subtypes. Our approach aims to consider type correct as many expressions as possible, and does not require data flow analysis. Thus it should be suitable for type checking legacy software, and should provide an appropriate alternative to the current suggestions for type checking Eiffel. However, it operates under the closed world assumption, ie. subclasses defined in separately compiled modules would invalidate any previously type checked modules importing the superclass. ST&T, a static type system for Smalltalk was developed, and implemented as a browser extension for Smalltalk. In this paper we prove the soundness of our approach. We introduce $\lambda^{\&,S}$, a syntax based on $\lambda^{\&}$, which reflects the essentials of the language Smalltalk. We define the operational semantics and type rules for $\lambda^{\&,S}$. We demonstrate the soundness of the approach by proving the subject reduction theorem.

Further work includes developing parameterized types to describe container classes and possible extensions to higher order.

Abstract:: We present a calculus based on the view that it should be possible to define a subclass method by specifying only the way in which it differs from the superclass methods of the same name. The calculus is a polymorphic extension of the merge calculus in which late binding can be expressed. We show that multi-methods can be represented naturally from this viewpoint; multi-methods and single-methods can both be expressed as generic functions with one argument by Currying, and a generic function behaves like a multi-method or a single-method depending on the covariance or contravariance of the component functions.

Abstract:: We present a new predicative and decidable type system, called ML<, suitable for object-oriented languages with implicit polymorphism in the tradition of ML. Instead of using extensible records as a foundation for object-oriented extensions of functional languages, we propose to reinterpret classical datatype declarations as abstract and concrete class declarations, and to replace pattern-matching on run-time values by dynamic dispatch on run-time types. ML< is based on universally quantified polymorphic constrained types, where constraints are conjunctions of inequalities between monotypes built from extensible and partially ordered classes of type constructors. We show how this type system can be used to design programming languages retaining much of the ML spirit while integrating in a seamless fashion higher-order and object-oriented programming, dynamic dispatch on several arguments, and parametric polymorphism. We give type-checking rules for a small, explicitly typed functional language with methods, and show that the resulting system has decidable minimal typing. We discuss type inference for this language. We show how abstraction and encapsulation can be achieved by proper use of a module system. We give a type-checking algorithm and discuss its complexity. We conclude by a comparison with related type systems in the literature.

Abstract: This talk presents a type-theoretic foundation for object systems that include ``interface types'' and ``implementation types,'' in the process accounting for access controls such as C++ private, protected and public levels of visibility. The 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.

Abstract: Objective ML is a small practical extension of ML with objects and toplevel classes. It is fully compatible with ML; its type system is based on ML polymorphism, record types with polymorphic access, and a better treatment of type abbreviations. Objective ML allows for most features of object-oriented languages including multiple inheritance, methods returning self and binary methods. This demonstrates that objects can be added to strongly typed languages based on ML polymorphism.

Abstract: We describe a simple encoding of classes in Object ML (OML) using the Standard ML (SML) module system. We show how to mimic class-based implementation inheritance using an extension of Abadi and Cardelli's "pre-methods". We also show how to encode other various class-based features, such as static members, protected members, and multiple inheritance. Our thesis is that the rich scoping discipline provided by SML has enough power to encode various aspects of the class systems of C++ and other languages.

Abstract: Adding container objects (such as list objects) to polymorphic languages, particularly languages with type inference such as ML, faces serious technical obstacles. One problem is the fact that polymorphic functions are second-class in languages with type inference, otherwise type inference is undecidable. Another problem is that type-checking of container objects with recursive interfaces remains an open problem, even for explicitly typed languages.

A type system is presented that overcomes all of these problems. The type system provides first-class objects with polymorphic methods, subtyping, recursive object types, method override and method type specialization. At the heart of the approach is the use of primitive method types, higher-order polymorphism and object type constructors. The object calculus can be considered as a class-based version of the object system of Abadi & Cardelli, with self types. The type system motivates the addition of primitive objects to polymorphic languages with type inference: objects with polymorphic methods are not possible with approaches that encode objects using records, datatypes or universal types.

Abstract: This tutorial will review attempts to ascribe semantics to concurrent object-based languages using both operational (SOS) and translational (to process algebras) approaches. The two semantic approaches will be compared as to their usefulness for gaining an intuitive understanding of the COOL in question. Thus far there is nothing very novel but the light shed on issues such as granularity will be considered and a tentative link with Benjamin Pierce's tutorial will be a comment on some novel properties which might be captured with type inference. Furthermore the question of proving the soundness of some equivalences will be shown to be a non-trivial challenge using either semantics.

Abstract: The piece of work reported here originates from the design of a real concurrent and distributed object-oriented design language developed within Ericsson. Originally constructs for distribution and concurrency were missing from the language, making it necessary to call on operating system services to implement distributed applications. The goal of the project was to include support for these aspects in the language itself thereby enabling implementations on different operating system platforms. In this paper we concentrate on the formal definition of a small core fraction of the design language, which we name Erken, and on some simulation and prototyping activities based on the formal definition.

In our opinion the first and foremost motive to formally define the semantics of a programming language is to enable language proposals to be stated precisely at an early design phase. This facilitates discussions about language design by reducing the potential for confusion due to unclear ideas and specifications.

In this paper we describe the Erken semantics which is defined via a translation of language constructs into the pi-calculus. The translation has been implemented as a compiler from Erken to the pi-calculus. To enable experimentation with the semantics a compiler from the variant of the pi-calculus used in the translation to the concurrent functional programming language Facile was also implemented. Defining the compiler in two steps has the advantage that a change in the semantics, that is, in the translation function to the pi-calculus, only results in a change in the Erken to pi-calculus compiler, which is an easy task due to the fact the the compiler is a straightforward implementation of the translation.

Abstract: We present an approach to reasoning about actor programs on the base of temporal logic. Temporal logic is particularly appropriate for the specification of concurrent programs, but most known temporal logic proof systems for concurrent computations rely on imperative language constructs and static process topologies, ignoring, e.g., the creation of processes and the dynamic configuration of communication channels, which are crucial for actor systems or other concurrent object-oriented programming languages. After sketching the actor model and introducing a simple syntax for actor programs we describe a general temporal logic system and then adjust it to the describtion of actor computations.

Abstract: The Curry--Howard isomorphism, a fundamental property shared by many type theories, establishes a direct correspondence between programs and proofs. This suggests that the same structuring principles that ease programming be used to simplify proving as well.

To exploit object-oriented structuring mechanisms for verification, we extend the object-model of Pierce and Turner, based on the higher order typed lambda-calculus Fomegasub, with a proof component. By enriching the (functional) signature of objects with a specification, the methods and their correctness proofs are packed together in the objects. The uniform treatment of methods and proofs gives rise in a natural way to object-oriented proving principles | including inheritance of proofs, late binding of proofs, and encapsulation of proofs | as analogues to object-oriented programming principles.

We have used LEGO, a type-theoretic proof checker, to explore the feasibility of this approach. In particular, we have verified a small hierarchy of classes.

Abstract: The pi-calculus (Milner, Parrow and Walker, 1989) has gained a lot of attention over the past few years as a process algebra for mobile processes. Central to the pi-calculus is the notion of *name*. Two processes with acquaintance of a given name can use it to interact with each other. In the interaction, names may be exchanged and, in this way, a process can acquire the ability to communicate with other processes. A major strength of the pi-calculus is the rich algebraic theory. Type systems for the pi-calculus have been recently put forward (Pierce and Sangiorgi 1993, Honda and Vasconcelos 1993, Turner 1995, etc..), as developments of Milner's *sorting discipline*.

The notions of name and of mobility are also central in Object-Oriented programming: Objects refer to each other using names and, during computation, object acquaintances may change and new objects may be created.

In my talk I will report on some experiments with the pi-calculus as a metalanguage for the semantics of typed Object-Oriented languages. Another motivation for this work is testing the usefulness of pi-calculus type systems, and investigating their relationship to familiar types of programming languages.

I will present an interpretation of Abadi and Cardelli's first-order functional *Object Calculus* (OC) into a first-order typed pi-calculus. The interpretation validates the subtyping relation and the typing judgements of OC, and is computationally adequate. Types are necessary to justify certain algebraic laws for the pi-calculus which are important in the proof of computational adequacy of the translation.

If there is time, I will discuss modifications/extensions of this interpretation to handle the imperative OC and the second-order OC.

Abstract: We present an extension to basic type theory to allow a uniform construction of abstract data types (ADTs) having many of the properties of objects, including abstraction, subtyping, and inheritance. The extension relies on allowing type dependencies for function types to range over a well-founded domain. Using the propositions-as-types correspondence, abstract data types can be identified with logical theories, and proofs of the theories are the objects that inhabit the corresponding ADT.

Abstract: We define an extension of a second-order type system with records, subtyping and record concatenation. This system can model the most important concepts of object-oriented languages. The novelty in our approach is that concatenation is only permitted if the types on common fields agree. We give examples of how object-oriented concepts can be modeled and show how the system can be translated to a type system without subtyping.