@article{BeierleBoerger96_Journal_FAC_PartII,
   AUTHOR = "C. Beierle and E. B{\"{o}}rger",
   TITLE = "Refinement of a typed {WAM} extension  
            by polymorphic order-sorted types",
    JOURNAL = "Formal Aspects of Computing",
    VOLUME = 8,
    NUMBER = 5,
    YEAR = 1996,
    PAGES = "539--564",
    ABSTRACT = {We refine the mathematical specification of a WAM extension
to type-constraint logic programming given in 
[Beierle and Boerger 1996, in: {\em 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, Boerger 1996]
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.}}