Certified binary search tree on W-types
Gustavo Arengas

TL;DR
This paper introduces a new approach to certified programming by defining new types using well-founded types and applying these ideas to binary search trees, enhancing guarantees of program correctness.
Contribution
It develops a novel elimination rule for well-founded types and demonstrates its application to binary search trees for certified programming.
Findings
New elimination rule for well-founded types
Application to certified binary search trees
Potential for improved program correctness guarantees
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsData Management and Algorithms · Algorithms and Data Compression · Data Mining Algorithms and Applications
