ISO-PROLOG and the Warren Abstract Machine

• History and Survey of ASM modelling of logic programming languages. Abstract
• The original ASM models for Prolog and their final version for the ISO standard of 1995. Abstract.
• Modelling and analysing Set Predicates in ISO-Prolog. Abstract .
• Modelling and analysing Database Views for Prolog
• Modelling the WAM and a proven to be correct general scheme for constructing compilers from Prolog to Warren Abstract Machine code. Abstract
  
  For achieving this goal a Refinement Method has been introduced into ASM which takes care of orthogonal components of the WAM and thus make the specification as well as the correctness proof modular and extendible. Examples of such extensions are found in:

• the Protos Abstract Machine (see abstract ), where Prolog and the WAM are refined by abstract types,
• the full PAM(see abstract ), developed at IBM Germany, where the abstract types are refined by polymorphic order-sorted types, as they appear in Protos-L, and implemented in the WAM extension
• the Constraint Logic Arithmetical Machine CLAM, developed at IBM Yorktown Heights, implementing the constraint logic programming language CLP(R),
• Araujo's Prolog Distributed Processor,
• Kwon's machine which permits procedure definitions to be given a scope .

For machine (KIV, ISABELLE) checked versions of the PROLOG-to-WAM correctness proof see the work by Ahrendt, Pusch, and Schellhorn cited in the 1999 ASM survey , in particular Schellhorn 's PhD thesis.

For an application of the refinement method to imperative or object-oriented languages, with parallelism and non determinism, see the papers on modelling, and proving the correctness of the compilation, of Occam to Transputer Code and of Java to Java Virtual Machine Code.