Typed Prolog: A Semantic Reconstruction of the Mycroft-O'Keefe Type System

Mycroft and O'Keefe [25] presented a declaration-based type system for Pro-log. However, they did not clarify the semantics of the type system, leading to several criticisms being voiced against it. We propose that the language accepted by this type system be viewed as a typed variant of Prolog, called Typed Prolog. We dene the formal semantics of Typed Prolog along the lines of many-sorted logic and polymorphic lambda calculus. Typed Prolog also supports a form of type inference called type reconstruction which takes a Typed Prolog program with missing type declarations, and reconstructs the most general type declarations satisfying the language denition. This approach contrasts with the inference based type systems which have been widely pursued heretofore.