Type inference in Prolog: a new approach

AbstractThis paper presents a new approach to type inference of Prolog programs. The novelty is in the fact that we only require the existence of a type domain T with a few primitive operations such as the abstract unificiation of elements of T, and operations allowing the construction and the extraction of types. We focus on the derivation of accurate sharing information that we prove correct. The derivation process is designed as an application of a recent method for global analysis for logic programs, formalized by an abstract interpretation framework. The framework ensures correctness and termination of the inferred properties if certain requirements are satisfied