Item

Abstract

In this chapter, we propose a framework for logic programming with different
type systems. In this framework a typed logic program consists of a type
specification and a Horn clause program which is well-typed with respect to the
type specification. The type specification defines all types which can be used
in the logic program. Relations between types are expressed by equations on the
level of types. This permits the specification of many-sorted, order-sorted,
polymorphic and polymorphically order-sorted type systems. We present the
declarative semantics of our framework and two proof procedures (deduction and
resolution) for typed logic programs. An interesting application is a type
system that combines parametric polymorphism with order-sorted typing and
permits higher-order logic programming. Moreover, our framework sheds some new
light on the r\^{o}le of types in logic programming.