Int. Conf. on Logic Programming, July 1997, Leuven
Tutorial on Types in Logic Programming
Gregor Meyer
Abstract:
An overwhelming number of approaches combining types with LP
proves the advantages of a typed declarative language.
On the other hand a general framework, or moreover a commonly
accepted base line for type systems in LP is missing.
In contrast, for procedural and functional languages such a
common base seems to be available. For example, in these languages
the concept of a type error is rather clear, the main purpose
of typing is to ensure program execution to be free from type errors,
and the semantics of a program is usually independent of types.
The tutorial clarifies how typed LP languages differ on these
aspects, notably on the definition of a type error.
Additional facets are explained, e.g., types as constraints
and the concept of useless expressions. As a central theme
we will elaborate three almost independent dimensions of
types in logic programming: types as approximations,
types as constraints and types for proving partial correctness.
Several type systems will be analyzed along these dimensions,
exhibiting their respective benefits and limitations.
GM May.'97,