Specifying and Verifying a Transformation of Recursive Functions into Tail-Recursive Functions. - Axel Suárez Polo; José de Jesús Lavalle-Martínez; Iván Molina Rebolledo (Computación y Sistemas (CyS), 2023)