C. Beierle and E. Börger. Refinement of a typed WAM extension by polymorphic order-sorted types. Formal Aspects of Computing, 8(5):539-564, 1996.
We refine the mathematical specification of a WAM extension to type-constraint logic programming given in [Beierle and Börger 1996, in: Formal Aspects of Computing, Vol. 8(4)]. We provide a full specification and correctness proof of the PROTOS Abstract Machine (PAM), an extension of the WAM by polymorphic order-sorted unification as required by the logic programming language PROTOS-L, by refining the abstract type constraints used in [Beierle and Börger 1996, in: Formal Aspects of Computing, Vol. 8(4)] to the polymorphic order-sorted types of PROTOS-L. This allows us to develop a detailed and 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.