Logic Programming over Polymorphically Order-Sorted Types

This thesis presents the foundations for relational logic programming over polymorphically order-sorted data types. This type discipline combines the notion of parametric polymorphism, which has been developed for higher-order functional programming, with the notion of order-sorted typing, which has been developed for equational first-order specification and programming. Polymorphically order-sorted types are obtained as canonical models of a class of specifications in a suitable logic accommodating sort functions. Algorithms for constraint solving, type checking and type inference are given and proven correct