F. Kamareddine, F. Monin, y M. Ayala Rincón, «On automating the extraction of programs from termination proofs», Rev. colomb. comput., vol. 4, n.º 2, pp. 1–20, dic. 2003.