A bargain for mergesorts -- How to prove your mergesort correct and stable, almost for free
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866913989327323136 |
|---|---|
| author | Cohen, Cyril Sakaguchi, Kazuhiko |
| author_facet | Cohen, Cyril Sakaguchi, Kazuhiko |
| contents | We present a novel characterization of stable mergesort functions using relational parametricity, and show that it implies the functional correctness of mergesort. As a result, one can prove the correctness of several variations of mergesort (e.g., top-down, bottom-up, tail-recursive, non-tail-recursive, smooth, and non-smooth mergesorts) by proving the characteristic property for each variation. Thanks to our characterization and the parametricity translation, we deduced the correctness results, including stability, of various implementations of mergesort for lists, including highly optimized ones, in the Rocq Prover (formerly the Coq Proof Assistant). |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2403_08173 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | A bargain for mergesorts -- How to prove your mergesort correct and stable, almost for free Cohen, Cyril Sakaguchi, Kazuhiko Logic in Computer Science Data Structures and Algorithms Programming Languages We present a novel characterization of stable mergesort functions using relational parametricity, and show that it implies the functional correctness of mergesort. As a result, one can prove the correctness of several variations of mergesort (e.g., top-down, bottom-up, tail-recursive, non-tail-recursive, smooth, and non-smooth mergesorts) by proving the characteristic property for each variation. Thanks to our characterization and the parametricity translation, we deduced the correctness results, including stability, of various implementations of mergesort for lists, including highly optimized ones, in the Rocq Prover (formerly the Coq Proof Assistant). |
| title | A bargain for mergesorts -- How to prove your mergesort correct and stable, almost for free |
| topic | Logic in Computer Science Data Structures and Algorithms Programming Languages |
| url | https://arxiv.org/abs/2403.08173 |