Deriving Sorting Algorithms
Jos\'e Bacelar Almeida, Jorge Sousa Pinto

TL;DR
This paper introduces a novel derivation method for three classic sorting algorithms using functional programming, combining algebraic transformations, inductive-coinductive reasoning, and structural invariants.
Contribution
It presents a new derivation approach that simplifies sorting algorithms from specifications through program transformations and algebraic reasoning.
Findings
Derived three well-known sorting algorithms functionally
Unified inductive and coinductive reasoning in derivations
Enhanced correctness proofs with structural invariants
Abstract
This paper proposes new derivations of three well-known sorting algorithms, in their functional formulation. The approach we use is based on three main ingredients: first, the algorithms are derived from a simpler algorithm, i.e. the specification is already a solution to the problem (in this sense our derivations are program transformations). Secondly, a mixture of inductive and coinductive arguments are used in a uniform, algebraic style in our reasoning. Finally, the approach uses structural invariants so as to strengthen the equational reasoning with logical arguments that cannot be captured in the algebraic framework.
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
Topicssemigroups and automata theory · Advanced Algebra and Logic · Algorithms and Data Compression
