Biernacka, M., O. Danvy, and K. Støvring. “Program Extraction from Proofs of Weak Head Normalization”. BRICS Report Series, vol. 12, no. 12, Apr. 2005, doi:10.7146/brics.v12i12.21878.