Refinement of a typed WAM extension by polymorphic order-sorted types

1 September 1996

journal article
research article
Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing

Vol. 8 (5) , 539-564
https://doi.org/10.1007/bf01211908

Abstract

We refine the mathematical specification of a WAM extension to typeconstraint logic programming given in [BeB96]. 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 [BeB96] 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.

Keywords

This publication has 7 references indexed in Scilit:

Specification and correctness proof of a WAM extension with abstract type constraints
Formal Aspects of Computing, 1996
Run-time type computations in the Warren Abstract machine
The Journal of Logic Programming, 1994
Logic programming with typed unification and its realization on an abstract machine
IBM Journal of Research and Development, 1992
Horn clause programs with polymorphic types: semantics and resolution
Theoretical Computer Science, 1991
Warren's Abstract Machine
Published by MIT Press ,1991
Logic programming with polymorphically order-sorted types
Lecture Notes in Computer Science, 1988
A polymorphic type system for prolog
Artificial Intelligence, 1984