M. Biernacka, O. Danvy, og K. Støvring, “Program Extraction from Proofs of Weak Head Normalization”, BRICS, bd. 12, nr. 12, apr. 2005.