  Types in logic programming have focused on conservative approximations of
program semantics by regular types, on one hand, and on type systems based on a
prescriptive semantics defined for typed programs, on the other. In this paper,
we define a new semantics for logic programming, where programs evaluate to
true, false, and to a new semantic value called wrong, corresponding to a
run-time type error. We then have a type language with a separated semantics of
types. Finally, we define a type system for logic programming and prove that it
is semantically sound with respect to a semantic relation between programs and
types where, if a program has a type, then its semantics is not wrong. Our work
follows Milner's approach for typed functional languages where the semantics of
programs is independent from the semantic of types, and the type system is
proved to be sound with respect to a relation between both semantics.
