A Formalisation of Algorithms for Sorting Network
Data Structures and Algorithms
2022-03-04 v1
Authors:
Laurent Théry
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.
Keywords
Cite
@article{arxiv.2203.01579,
title = {A Formalisation of Algorithms for Sorting Network},
author = {Laurent Théry},
journal= {arXiv preprint arXiv:2203.01579},
year = {2022}
}
Related papers
View all related →
Logic in Computer Science · Computer Science
Revisiting the Fast Fourier Transform in Rocq
Laurent Théry
2025-08-15
Logic in Computer Science · Computer Science
Formalizing Higher-Order Termination in Coq
Deivid Vale, Niels van der Weide
2021-12-14
Logic in Computer Science · Computer Science
Machine-Checked Categorical Diagrammatic Reasoning
Benoît Guillemet, Assia Mahboubi, Matthieu Piquerez
2024-03-01
Logic in Computer Science · Computer Science
Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
Assia Mahboubi, Cyril Cohen
2015-07-01
Logic in Computer Science · Computer Science
Mechanizing Matching Logic In Coq
Péter Bereczky, Xiaohong Chen, Dániel Horpácsi, Lucas Peña +1
2022-09-22
Logic in Computer Science · Computer Science
Taming Differentiable Logics with Coq Formalisation
Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Ślusarz +1
2024-07-08
Logic in Computer Science · Computer Science
Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant
Théo Zimmermann, Hugo Herbelin
2015-07-10
History and Overview · Mathematics
Experimental library of univalent formalization of mathematics
Vladimir Voevodsky
2014-07-01
Logic in Computer Science · Computer Science
Formalized linear algebra over Elementary Divisor Rings in Coq
Guillaume Cano, Cyril Cohen, Maxime Dénès, Anders Mörtberg +1
2019-03-14
Logic in Computer Science · Computer Science
Coinductive Formal Reasoning in Exact Real Arithmetic
Milad Niqui
2015-07-01
Programming Languages · Computer Science
MirrorShard: Proof by Computational Reflection with Verified Hints
Gregory Malecha, Adam Chlipala, Thomas Braibant, Patrick Hulin +1
2013-05-29
Distributed, Parallel, and Cluster Computing · Computer Science
A Framework for Certified Self-Stabilization
Karine Altisen, Pierre Corbineau, Stephane Devismes
2023-06-22
Software Engineering · Computer Science
Plotting in a Formally Verified Way
Guillaume Melquiond
2021-08-10
Logic in Computer Science · Computer Science
Developments in Formal Proofs
Thomas C. Hales
2014-08-28
Logic in Computer Science · Computer Science
Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs
Yves Bertot
2018-09-05
Programming Languages · Computer Science
A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms
Chengxi Yang, Shushu Wu, Qinxiang Cao
2025-05-01
Programming Languages · Computer Science
Validating Mathematical Structures
Kazuhiko Sakaguchi
2020-09-22
Logic in Computer Science · Computer Science
Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker
Luís Cruz-Filipe, Peter Schneider-Kamp
2016-11-30
Distributed, Parallel, and Cluster Computing · Computer Science
Formally Proving and Enhancing a Self-Stabilising Distributed Algorithm
Camille Coti, Charles Lakos, Laure Petrucci
2016-01-18
Logic in Computer Science · Computer Science
Towards a Coq formalization of a quantified modal logic
Ana de Almeida Borges
2023-12-20
Logic in Computer Science · Computer Science
Reliably Reproducing Machine-Checked Proofs with the Coq Platform
Karl Palmskog, Enrico Tassi, Théo Zimmermann
2022-03-21
Logic in Computer Science · Computer Science
Theorem proving support in programming language semantics
Yves Bertot
2007-07-10
Logic in Computer Science · Computer Science
Formalizing May's Theorem
Kwing Hei Li
2022-10-12
Programming Languages · Computer Science
Accelerating Verified-Compiler Development with a Verified Rewriting Engine
Jason Gross, Andres Erbsen, Jade Philipoom, Rajashree Agrawal +1
2025-03-12
Computational Geometry · Computer Science
Computer Aided Formal Design of Swarm Robotics Algorithms
Thibaut Balabonski, Pierre Courtieu, Robin Pelle, Lionel Rieg +2
2021-01-19