A SEMANTICS FOR STATIC TYPE INFERENCE

Curry's system for F-deducibility is the basis for static type inferen ce algorithms for programming languages such as ML. If a natural ''pre servation of types by conversion'' rule is added to Curry's system, it becomes undecidable, but complete relative to a variety of model clas ses. We show completeness for Curry's system itself, relative to an ex tended notion of model that validates reduction but not conversion. Tw o proofs are given: one uses a term model and the other a model built from type expressions. Extensions to systems with polymorphic or inter section types are also considered. (C) 1994 Academic Press, Inc.