Abstracts
Abstract: Cliff Jones has raised the challenge of how to prove the validity of a certain transformation that increases the concurrent activity in a system of concurrent objects. We present a proof of this transformation that uses a typed pi-calculus and typed behavioural equivalences. Our type system is that for receptiveness; it guarantees that the input-end of certain channels is always ready to receive messages (at least as long as there are processes that could send such messages), and that all messages will be processed using the same continuation. This work is also intended as an example of the usefulness of pi-calculus types for reasoning.
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.
Abstract: Amidst rocketing numbers of enthusiastic Java programmers and internet applet users, there is growing concern about the security of executing Java code produced by external, unknown sources. Rather than waiting to find out empirically what damage Java programs do, we aim to examine first the language and then the environment looking for points of weakness. A proof of the soundness of the Java type system is a first, necessary step towards demonstrating which Java programs won't compromise computer security.
We argue that the Java type system is sound, by proving a subject reduction theorem. We define a subset of Java, a language which is safe and which reflects the most essential features of Java, a term rewriting system for the operational semantics and a type inference system to describe compile time type checking. We prove that program execution preserves the types, up to the subclass/subinterface relationship.
Abstract: In this paper we present a modal logic for describing properties of terms in the object calculus of Abadi and Cardelli. The logic is essentially the modal mu-calculus of Kozen. The fragment allows us to express the temporal modalities of the logic CTL. We investigate the connection between a recursive type system for the object calculus and the mu-calculus, providing a translation of types into modal formulae and an ordering on formulae that is sound w.r.t. to the subtype ordering of the type system.
Abstract: Abadi and Cardelli have presented and investigated object calculi that model most object-oriented features found in actual object-oriented programming languages. The calculi are innate object calculi in that they are not based on lambda-calculus. They present a series of type systems for their calculi, four of which are first-order. Palsberg has shown how typability in each one of these systems can be decided in time O(n^3), where n is the size of an untyped object expression, using an algorithm based on dynamic transitive closure. He also shows that each of the type inference problems is hard for polynomial time under log-space reductions.
In this paper we show how we can break through the ``dynamic transitive closure bottleneck'' and improve each one of the four type inference problems from O(n^3) to the following time complexities:
Ob1 (no subtyping/no rec. types): O(n) Ob1mu (no subtyping/rec. types): O(n log^2 n) Ob1< (subtyping/no rec. types): O(n^2) Ob1<mu (subtyping/rec. types): O(n^2)The key ingredient that lets us ``beat'' the worst-case time complexity induced by using general dynamic transitive closure or similar algorithmic methods is that object subtyping is invariant: an object type is a subtype of a ``shorter'' type with a subset of the field names if and only if the common fields have equal types.
Abstract: In this paper we present a general framework HM(X) for Hindley/Milner style type systems with constraints. We give a generic type inference algorithm for HM(X). Under sufficient conditions on X, type inference will always compute the principal type of a term. We give an extension of our HM(X) systems which deals with subtyping. In particular, the type inference algorithm for subtypes computes principal types. Simplification of the constraints inferred by the type inference algorithm is discussed in general for HM(X) and in the special case of subtyping.
Abstract: This paper describes a small object-oriented programming language and its axiomatic semantics. The language includes common object-oriented features like methods and subtyping. Objects are implicitly references, and the semantics handles the aliasing that arises. The paper formalizes in first-order logic what it means for a method implementation to meet its specification.
Abstract: We present and analyze the semantics and static type system for BeCecil, a theoretical (core) language with multimethods. BeCecil is a simple and orthogonal version of object-oriented languages like Cecil, CLOS, and Dylan. BeCecil has a new, simple mechanism for information hiding, which allows subclassing and yet can preserve representation invariants. BeCecil is also block-structured; within a block, one can extend a generic function with new multimethods, which may come from other generic functions. The inheritance relationships of objects may be extended in any block, and are statically scoped. The type system separates classes from types, and inheritance from subtyping. Subtype relationships are also extensible and statically scoped. These features combine to make BeCecil unusually expressive, while still allowing static typechecking.
Return to the FOOL 4 home page.