Browse Theses

We design new type expressions and algorithms to classify and check object types in higher-order programming. Our computation model is imperative and strongly typed. It has dynamic-dispatched functions, higher-order bounded polymorphic functions, record and function subtyping, parameterized types, both named and structural types, free-union types, existential union types, poly-typed variables, poly-typed expressions, and heterogeneous collections.

A prototype of a mini-language with the above features is implemented in Prolog with a type checking system. A small but powerful set of typing structures and operations is identified. The type checking rules are formally defined. A new technique is developed for translating recursive type relations into cyclic AND/OR graphs. Efficient algorithms are designed for resolving generalized AND/OR graphs with constraints on valid cycles.

Using elegant syntax the new type system describes more general and precise type relations than any other type systems we have known. The new technique for translating type relations into AND/OR graphs provides a new direction for implementing a higher-order polymorphic type system, which is not available in unification-based type systems. The AND/OR graph models are general enough to represent recursive relations, and their applications are not solely limited to type-checking. Our AND/OR graph resolution algorithms find the optimal solutions. They are theoretically proved efficient and are shown practical in our implementation.