Proof Pearl: The KeY to Correct and Stable Sorting
The work
| Title | Proof Pearl: The KeY to Correct and Stable Sorting |
|---|---|
| Authors | Stijn de Gouw; Frank S. de Boer; Jurriaan Rot |
| Type | article |
| Year | 2014 |
| Citekey | gouw2014proof |
Where it appeared
| Published in | Journal of Automated Reasoning |
|---|---|
| Publisher | Springer |
| Volume | 53 |
| Issue | 2 |
| Pages | 129--139 |
Identifiers
| DOI | 10.1007/s10817-013-9300-y |
|---|---|
| OpenAlex | W1998392058 |
Access
| Landing page | https://doi.org/10.1007/s10817-013-9300-y |
|---|---|
| Free full text | https://ir.cwi.nl/pub/23074 |
Abstract
We discuss a proof of the correctness of two sorting algorithms: Counting sort and Radix sort. The semi-automated proof is formalized in the state-of-the-art theorem prover KeY.
Copy held
| Kind | PDF, 306.5 kB |
|---|---|
| Retrieved | 2026-08-08 |
| Held | local, for personal reference |
| Where it came from | https://ir.cwi.nl/pub/23074/23074D.pdf |
Where this came from
| How it got here | the agent went looking · found via openalex |
|---|---|
| First seen | 2026-08-04 |
| Record | reviewed by a person |
| Approved | 2026-08-16 |
Cite it as
@article{gouw2014proof,
title = {Proof Pearl: The KeY to Correct and Stable Sorting},
author = {Stijn de Gouw and Frank S. de Boer and Jurriaan Rot},
year = {2014},
journal = {Journal of Automated Reasoning},
volume = {53},
number = {2},
pages = {129--139},
publisher = {Springer},
doi = {10.1007/s10817-013-9300-y},
url = {https://ir.cwi.nl/pub/23074},
}
This record lives at https://refs.drheap.org/gouw2014proof/ and will keep doing so.