Certified binary search tree on W-types
Fuente:
arXiv
Enregistré dans:
| Auteur principal: | |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866909374424809472 |
|---|---|
| author | Arengas, Gustavo |
| author_facet | Arengas, Gustavo |
| contents | Software bugs have caused enormous economic and human loss in recent years. Certified programming seeks to solve this problem by developing languages where we can make demonstrations that guarantee that our programs work properly. However, the rapid evolution of modern algorithms constantly forces us to develop new tools for this task. In this article we explore the possibility of defining new types using well-founded types. In particular, we developed a new elimination rule on the terms of the type. We apply these ideas to binary search trees to illustrate the power of the method. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_00242 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Certified binary search tree on W-types Arengas, Gustavo Software Engineering Data Structures and Algorithms Category Theory Software bugs have caused enormous economic and human loss in recent years. Certified programming seeks to solve this problem by developing languages where we can make demonstrations that guarantee that our programs work properly. However, the rapid evolution of modern algorithms constantly forces us to develop new tools for this task. In this article we explore the possibility of defining new types using well-founded types. In particular, we developed a new elimination rule on the terms of the type. We apply these ideas to binary search trees to illustrate the power of the method. |
| title | Certified binary search tree on W-types |
| topic | Software Engineering Data Structures and Algorithms Category Theory |
| url | https://arxiv.org/abs/2411.00242 |