An Experiment in Type Inference and Verification by Abstract Interpretation

This paper describes an experiment in the definition of tools for type inference and type verification of ML-like functional languages, using abstract interpretation techniques. We first show that by extending the Damas-Milner type inference algorithm, with a (bounded) fixpoint computation (as suggested by the abstract interpretation view, i.e. by a slight variation of one of the type abstract semantics in [7]), we succeed in getting a better precision and solving some problems of the ML type inference algorithm without resorting to more complex type systems (e.g