Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof

DOI10.1007/978-3-319-20615-8_4zbMath1417.68180arXiv1502.08008OpenAlexW1537750720MaRDI QIDQ3453106

Luís Cruz-Filipe, Peter Schneider-Kamp

Publication date: 20 November 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1502.08008

Mathematics Subject Classification ID

Searching and sorting (68P10)

Related Items (3)

Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker ⋮ Formally proving size optimality of sorting networks ⋮ Sorting nine inputs requires twenty-five comparisons

Uses Software

• Coq
• CiME

Cites Work

• 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
• Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker
• 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
• Formalizing Bounded Increase

This page was built for publication: Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof