ISO-PROLOG and the Warren Abstract Machine

• History and Survey of ASM modelling of logic programming languages using ASMs
• Boerger's original ASM models for Prolog (1990-92) became the ISO-Prolog  model: SCP 24 (1995) 249--286
• Modelling and analysing Set Predicates in ISO-Prolog
• Modelling and analysing Database Views for Prolog: Springer LNCS 528 (1991) 147-185
• Modelling the WAM and a proven to be correct general scheme for constructing compilers from Prolog to Warren Abstract Machine code.
  
  For achieving this goal a Refinement Method  has been introduced into ASM which takes care of orthogonal components of the WAM and thus makes the specification as well as the correctness proof modular and extendible. Examples of such modular extensions of the WAM by ASM refinements are the following:

• IBM's Protos Abstract Machine   (IBM Germany) where Prolog and the WAM are refined by abstract types (see abstract)
• full PAM where the abstract types are refined by polymorphic order-sorted types, as they appear in Protos-L, and implemented in the WAM extension (see abstract)
• IBM's Constraint Logic Arithmetical Machine CLAM (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, 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 nondeterminism, 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.