*Abstract:*

In this thesis we study some of the problems which occur when
type inference is used in a type system with subtyping. An
underlying poset of atomic types is used as a basis for our
subtyping systems. We argue that the class of *Helly* posets
is of significant interest, as it includes lattices and trees, and
is closed under type formation not only with structural
constructors such as function space and list, but also records,
tagged variants, Abadi-Cardelli object constructors, top and bottom
. We develop a general theory relating consistency, solvability,
and solution of sets of constraints between regular types built
over Helly posets with these constructors, and introduce semantic
notions of simplification and entailment for sets of constraints
over Helly posets of base types. We extend Helly posets with
inequalities of the form `a` <= *tau*, where
*tau* is not necessarily atomic, and show how this enables us
to deal with bounded quantification.

Using bounded quantification we define a subtyping system which
combines structural subtype polymorphism and predicative parametric
polymorphism, and use this to extend with subtyping the type system
of Laufer and Odersky for ML with type annotations. We define a
complete algorithm which infers minimal types for our extension,
using *factorisations*, solutions of subtyping problems
analogous to principal unifiers for unification problems. We give
some examples of typings computed by a prototype
implementation.

**ECS-LFCS-98-403**.

This is a 149-page PhD thesis.

This report is available in the following formats:

- PDF file
- Gzipped PDF file
- PostScript file
- Gzipped PostScript file
- PostScript file with Type 1 fonts
- Gzipped PostScript file with Type 1 fonts
- LaTeX DVI file
- Gzipped LaTeX DVI file