Kamareddine, F. et al. 2003. On automating the extraction of programs from termination proofs. Revista Colombiana de Computación. 4, 2 (dic. 2003), 1–20.