Abstract

Abstract
Constructor subtyping is a form of subtyping in which an inductive type s is viewed as a subtype of another inductive type t if t has more constructors than s. As suggested in [5,12], its (potential) uses include proof assistants and functional programming languages. In this paper, we introduce and study the properties of a simply typed ?-calculus with record types and datatypes, and which supports record subtyping and constructor subtyping. In the first part of the paper, we show that the calculus is confluent and strongly normalizing. In the second part of the paper, we show that the calculus admits a well-behaved theory of canonical inhabitants, provided one adopts expansive extensionality rules, including ?-expansion, surjective pairing, and a suitable expansion rule for datatypes. Finally, in the third part of the paper, we extend our calculus with unbounded recursion and show that confluence is preserved. © Springer-Verlag Berlin Heidelberg 1999.

Abstract

Abstract
Constructor subtyping is a form of subtyping in which an inductive type sigma is viewed as a subtype of another inductive type tau if tau has more constructors than sigma. As suggested in [5, 12], its (potential) uses include proof assistants and functional programming languages. In this paper, we introduce and study the properties of a simply typed lambda-calculus with record types and datatypes, and which supports record subtyping and constructor subtyping. In the first part of the paper, we show that the calculus is confluent and strongly normalizing. In the second part of the paper, we show that the calculus admits a well-behaved theory of canonical inhabitants, provided one adopts expansive extensionality rules, including eta-expansion, surjective pairing, and a suitable expansion rule for datatypes. Finally, in the third part of the paper, we extend our calculus with unbounded recursion and show that confluence is preserved.

Abstract
This chapter contains summaries of the presentations given at the Intercontinental Workshop on Aliasjng in Object-Oriented Systems (IWAOOS'99) at the European Conference on Object-Oriented Programming (ECOOP'99) which was held in Lisbon, Portugal on June 15, 1999.

Abstract
Current data abstraction mechanisms are not adequate to control sharing of state in the general case involving objects in linked structures. The pervading possibility of sharing is a source of errors and an obstacle to language implementation techniques. Balloon types, which we have introduced in [2], are a general extension to programming languages. They make the ability to share state a first class property of a data type. The balloon invariant expresses a strong form of encapsulation: no state reachable (directly or transitively) by a balloon object is referenced by any external object. In this paper we describe the checking mechanism for balloon types. It relies on a non-trivial static analysis, described as an abstract interpretation. Here we focus in particular on the design of the abstract domain which allows the checking mechanism to work under realistic assumptions regarding possible object aliasing. ©1999 Published by Elsevier Science B. V.