M. Biernacka, O. Danvy, and K. Støvring, “Program Extraction from Proofs of Weak Head Normalization”, BRICS, vol. 12, no. 12, Apr. 2005.