O. Danvy, M. Rhiger, and K. H. Rose, “Normalization by Evaluation with Typed Abstract Syntax”, BRICS, vol. 8, no. 16, May 2001.