一句话：用关系参数性刻画稳定归并排序，使多种实现的正确性与稳定性证明在 Rocq 中近乎免费。
本文提出一种基于关系参数性（relational parametricity）的稳定归并排序函数刻画，并证明该刻画蕴含归并排序的函数正确性。由此，对某一归并排序变体只需证明其满足该特征性质，便可推出其正确性。作者利用该刻画与参数性翻译，在 Rocq Prover（原 Coq）中推导了多种列表归并排序实现的正确性与稳定性，包括自顶向下、自底向上、尾递归与非尾递归、平滑与非平滑以及高度优化的实现。该方法将正确性证明转化为对统一特征性质的验证，从而显著降低证明负担，实现“几乎免费”地证明归并排序正确且稳定。
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).
@article{paperbot3029,
title = {A Bargain for Mergesorts: How to Prove Your Mergesort Correct and Stable, Almost for Free},
author = {Cyril Cohen and Kazuhiko Sakaguchi},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {ICFP},
year = {2025},
doi = {10.1145/3747505}
}