Formal Specification of a Prolog Compiler

by Michael Hanus

International Workshop on Programming Language Implementation and Logic Programming (PLILP'88), Springer LNCS 348, pp. 273-282, 1988
© Springer-Verlag

This paper presents an outline of a formal specification of a compiler and a virtual machine for the programming language Prolog. The specification of the compiler can be transformed into an equivalent Prolog program. The specification of the virtual machine is the basis of an implementation of the virtual machine as an interpreter written in a low-level language. Moreover, the specification may be used for correctness proofs of a Prolog system.

DVI (34 KB) Postscript (146 KB) BibTeX-Entry