Zena_M.__Ariola
and Arvind. Properties of a first-order functional language with sharing
Correctness of monadic state: an imperative call-by-need calculus
Cyclic lambda graph rewriting
Relating graph and term rewriting via Bohm models. Applicable Algebra