ISO-PROLOG and the Warren Abstract Machine


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.