Formally proving size optimality of sorting networks

DOI10.1007/s10817-017-9405-9zbMath1425.68372OpenAlexW2584482282MaRDI QIDQ1694569

Kim S. Larsen, Peter Schneider-Kamp, Luís Cruz-Filipe

Publication date: 2 February 2018

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-017-9405-9

zbMATH Keywords

program extractioninteractive theorem provingsorting networkslarge-scale proofs

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Related Items (2)

How to get more out of your oracles ⋮ Formally verifying the solution to the Boolean Pythagorean triples problem

Uses Software

• Coq
• Isabelle/HOL
• HOL Light
• CoLoR
• CiME

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Sorting nine inputs requires twenty-five comparisons
• Bounds on the size of test sets for sorting and related networks
• The four color proof suffices
• Preserving order in a forest in less than logarithmic time and linear space
• Every planar map is four colorable. I: Discharging
• Every planar map is four colorable. II: Reducibility
• A Skeptic's approach to combining HOL and Maple
• Isabelle/HOL. A proof assistant for higher-order logic
• Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22--26, 2013. Proceedings
• Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
• Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates
• A SAT Attack on the Erdős Discrepancy Conjecture
• A computer-assisted optimal depth lower bound for nine-input sorting networks
• Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof
• Extraction in Coq: An Overview
• Certified Exact Transcendental Real Number Computation in Coq
• Toward a Lower Bound for Sorting Networks
• Computer Certified Efficient Exact Reals in Coq
• Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation
• Formalizing Bounded Increase
• Optimal Sorting Networks
• Theorem Proving in Higher Order Logics
• The NP-completeness column: An ongoing guide

This page was built for publication: Formally proving size optimality of sorting networks