A. Finlay and L. Allison, ACM Trans. Prog. Langs. and Systems, 15(1), pp.206-208, doi:10.1145/151646.151652, Jan. 1993

In [1] we described the use of Standard ML[2] to implement and experiment with the denotational semantics of Prolog[3]. In the process of implementing the semantics, an error was detected by the Standard ML type system. As well as providing a correction to the semantics, this note is of interest as a demonstration of the advantage of implementing semantics in a strongly typed functional programming language. The error occurs consistently throughout the semantics wherever unify is applied, except in its own definition. ...

paper: [doi:10.1145/151646.151652]['08]