@article{BeierleBoerger96_Journal_FAC,
AUTHOR = "C. Beierle and E. B{\"{o}}rger",
TITLE = "Specification and correctness proof of a {WAM} extension
for type-constraint logic programming",
JOURNAL = "Formal Aspects of Computing",
VOLUME = 8,
NUMBER = 4,
YEAR = 1996,
PAGES = "428--462",
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 \mbox{PROTOS-L}.
\\ \hspace*{0.5cm}
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\"{o}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\"{o}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.
\\ \hspace*{0.5cm}
In the second part of the paper, we refine the type constraints to
the polymorphic order-sorted types of \mbox{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.}}