| Journal: | Computación y sistemas |
| Database: | |
| System number: | 000560763 |
| ISSN: | 1405-5546 |
| Authors: | Suárez Polo, Axel1 Lavalle Martínez, José de Jesús1 Molina Rebolledo, Iván1 |
| Institutions: | 1Benemérita Universidad Autónoma de Puebla, Puebla, México |
| Year: | 2023 |
| Season: | Ene-Mar |
| Volumen: | 27 |
| Number: | 1 |
| Pages: | 333-340 |
| Country: | México |
| Language: | Inglés |
| English abstract | It is well known that some recursive functions admit a tail recursive counterpart which have a more efficient time-complexity behavior. This paper presents a formal specification and verification of such process. A monoid is used to generate a recursive function and its tail-recursive counterpart. Also, the monoid properties are used to prove extensional equality of both functions. In order to achieve this goal, the Agda programming language and proof assistant is used to generate a parametrized module with a monoid, via dependent types. This technique is exemplified with the length, reverse, and indices functions over lists. |
| Keyword: | Dependent types, Formal specification and verification, Tail recursion, Accumulation, Program transformation |
| Full text: | Texto completo (Ver HTML) Texto completo (Ver PDF) |
