Regular Types for Active Objects

Previous work on type-theoretic foundations for object-oriented programming languages has mostly focussed on applying or extending functional type theory to functional "objects." This approach, while benefitting from a vast body of existing literature, has the disadvantage of dealing with state change either in a roundabout way or not at all, and completely sidestepping issues of concurrency. In particular, dynamic issues of non-uniform service availability and conformance to protocols are not addressed by functional types. We propose a new type framework that characterizes objects as regular (finite state) processes that provide guarantees of service along public channels. We also propose an original notion of subtyping for regular types that extends Wegner and Zdonik's "principle of substitutability" to non-uniform service availability, and we relate it to known process equivalences. Finally, we formalize what it means to "satisfy a client's expectations," and we show how regular typ..