A Formalisation of Algorithms for Sorting Network
Laurent Th\'ery (STAMP)
TL;DR
This paper formalizes standard sorting network algorithms and proves their correctness within the Coq proof assistant, enhancing confidence in their implementation through formal verification.
Contribution
It introduces a formalization and correctness proof of sorting network algorithms using Coq and SSReflect, which was not previously documented.
Findings
Algorithms are formally verified in Coq.
Proof of correctness for sorting network algorithms.
Enhances reliability of sorting network implementations.
Abstract
This notes explains how standard algorithms that construct sorting networks have been formalised and proved correct in the Coq proof assistant using the SSReflect extension.
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
TopicsLogic, programming, and type systems · Distributed systems and fault tolerance · Formal Methods in Verification