A. Filinski and H. K. Rohde, “A Denotational Account of Untyped Normalization by Evaluation”, BRICS, vol. 10, no. 40, Dec. 2003.