Formally proving size optimality of sorting networks
type: Item
instance of: scholarly article
title: Formally proving size optimality of sorting networks
zbMATH Open document ID: 1425.68372
author: Luís Cruz-Filipe
author: Kim S. Larsen
author: Peter Schneider-Kamp
published in: Journal of Automated Reasoning
publication date: 2018-02-02T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68N18
Mathematics Subject Classification ID: 68Q17
Mathematics Subject Classification ID: 68Q25
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 6833657
zbMATH Keywords: interactive theorem proving
zbMATH Keywords: large-scale proofs
zbMATH Keywords: program extraction
zbMATH Keywords: sorting networks
describes a project that uses: Coq
describes a project that uses: Isabelle/HOL
describes a project that uses: HOL Light
describes a project that uses: CoLoR
describes a project that uses: CiME
MaRDI profile type: Publication
full work available at URL: s10817-017-9405-9
OpenAlex ID: W2584482282
cites work: Every planar map is four colorable. I: Discharging
cites work: The four color proof suffices
cites work: Every planar map is four colorable. II: Reducibility
cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
cites work: CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates
cites work: Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22--26, 2013. Proceedings
cites work: Optimal Sorting Networks
cites work: Bounds on the size of test sets for sorting and related networks
cites work: Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation
cites work: Sorting nine inputs requires twenty-five comparisons
cites work: Q5389068
cites work: A large-scale experiment in executing extracted programs
cites work: Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker
cites work: Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof
cites work: Theorem Proving in Higher Order Logics
cites work: Q5302559
cites work: Q5675725
cites work: A Skeptic's approach to combining HOL and Maple
cites work: Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
cites work: The NP-completeness column: An ongoing guide
cites work: Q4057549
cites work: A SAT Attack on the Erdős Discrepancy Conjecture
cites work: Computer Certified Efficient Exact Reals in Coq
cites work: Extraction in Coq: An Overview
cites work: Q4736399
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Certified Exact Transcendental Real Number Computation in Coq
cites work: Q4457464
cites work: A computer-assisted optimal depth lower bound for nine-input sorting networks
cites work: Formalizing Bounded Increase
cites work: Preserving order in a forest in less than logarithmic time and linear space
cites work: Toward a Lower Bound for Sorting Networks
DOI: 10.1007/S10817-017-9405-9
Recommended article: Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker
Recommended article: New Bounds on Optimal Sorting Networks
Recommended article: Optimal Sorting Networks
Recommended article: Q4234092
Recommended article: Toward a Lower Bound for Sorting Networks
Recommended article: Optimal-depth sorting networks
Recommended article: On optimal parallelization of sorting networks
Recommended article: Q3771637
Recommended article: Single-exception sorting networks and the computational complexity of optimal sorting network verification
Recommended article: On the complexity of min-max sorting networks
description: scientific article; zbMATH DE number 6833657