Ian A. Mason. Equivalence of First Order LISP Programs. Proving Properties of Destructive Programs via Transformation. In Proceedings, Symposium on Logic in Computer Science, 16-18 June 1986, Cambridge, Massachusetts, USA. pages 105-117, IEEE Computer Society, 1986.