We present a denotational continuation semantics for PROLOG with cut. First a uniform language B is studied, which captures the control flow aspects of PROLOG. The denotational semantics for B is proven equivalent to a transition system based operational semantics. The congruence proof relies on the representation of the operational semantics as a chain of approximations and on a convenient induction principle. Finally, we interpret the abstract language B such that we obtain equivalent denotational and operational models for PROLOG itself.

PROLOG, abstract language B, denotational continuation semantics
Erasmus School of Economics

de Bruin, A, & de Vink, E.P. (1989). Continuation semantics for PROLOG with cut. Retrieved from http://hdl.handle.net/1765/1507