The present paper represents a first step to a complete specification and correctness proof for the concrete PAM system ‒ an extension of the Warren Abstract Machine (WAM) by the polymorphic order-sorted unification. Section 2 describes the derivation of the PROTOS-L algebras (PROTOS-L language being a logic programming language based on PAM, introduced by the first author) from standard Prolog algebras (introduced by the second author). Section 3 defines PROTOS-L algebras with compiled AND/OR structure, while Section 4 introduces the representation of terms. Section 5 provides the stack representation of environments and choice- points, and gives the main result of the paper: For every such type- constraint logic programming system L, and for every compiler satisfying the specified conditions, the WAM extension with the abstract notion of types (thus PAM) is correct with respect to language L.
Reviewer: N.Curteanu (Iaşi)