Kamareddine, F.; Monin, F.; Ayala Rincón, M. On Automating the Extraction of Programs from Termination Proofs. Rev. colomb. comput. 2003, 4, 1-20.