C. Beierle and E. Börger.
**Specification and correctness proof of a WAM extension for type-constraint
logic programming**.
Formal Aspects of Computing, 8(4):428-462, 1996.

#### Abstract

We provide a mathematical specification of an extension of Warren's Abstract
Machine for executing Prolog to type-constraint logic programming and prove
its correctness. Our aim is to provide a full specification and correctness
proof of a concrete system, the PROTOS Abstract Machine (PAM), an extension of
the WAM by polymorphic order-sorted unification as required by the logic
programming language PROTOS-L.

In the first part of the paper, we keep the notion of types and dynamic type
constraints rather abstract to allow applications to different constraint
formalisms like Prolog III or CLP(R). This generality permits us to introduce
modular extensions of Börger's and Rosenzweig's formal derivation of the
WAM. Since the type constraint handling is orthogonal to the compilation of
predicates and clauses, we start from type-constraint Prolog algebras with
compiled AND/OR structure that are derived from Börger's and Rosenzweig's
corresponding compiled standard Prolog algebras. The specification of the
type-constraint WAM extension is then given by a sequence of evolving algebras,
each representing a refinement level, and for each refinement step a
correctness proof is given. Thus, we obtain the theorem that for every such
abstract type-constraint logic programming system L, every compiler to the WAM
extension with an abstract notion of types which satisfies the specified
conditions, is correct.

In the second part of the paper, we refine the type constraints to the
polymorphic order-sorted types of PROTOS-L. This allows us to develop a
detailed, yet due to the use of evolving algebras, mathematically precise
account of the PAM's compiled type constraint representation and solving
facilities, and to extend the correctness theorem to compilation on the fully
specified PAM.

Available:
PDF,
PS,
DVI,
BibTeX