We introduce a new semantics for logic programming languages. It generalises the traditional Herbrand universe semantics, and specialises the semantics of logical relations, as used in analysing parametricity in functional and imperative programming languages. We outline a typed logic programming language, give it this semantics, and show how it supports structured development of logic programs as advocated by Sterling et al. In particular, it gives semantics for some dynamic aspects of logic programs.
The first author acknowledges the support of MITI Cooperative Architecture Project.
he second author gratefully acknowledges the support of EPSRC grant GR/J84205 Frameworks for programming language semantics and logic.