Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof (Q3453106): Difference between revisions

@@ Property / OpenAlex ID @@
+W1537750720
@@ Property / OpenAlex ID: W1537750720 / rank @@
+Normal rank
@@ Property / arXiv ID @@
+.08008
@@ Property / arXiv ID: 1502.08008 / rank @@
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+Sorting nine inputs requires twenty-five comparisons
+Normal rank
@@ Property / cites work @@
+Q5389068
@@ Property / cites work: Q5389068 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2852042
@@ Property / cites work: Q2852042 / rank @@
+Normal rank
@@ Property / cites work @@
+Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker
+Normal rank
@@ Property / cites work @@
+Q5675725
@@ Property / cites work: Q5675725 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4057549
@@ Property / cites work: Q4057549 / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Certified Efficient Exact Reals in Coq
@@ Property / cites work: Computer Certified Efficient Exact Reals in Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Extraction in Coq: An Overview
@@ Property / cites work: Extraction in Coq: An Overview / rank @@
+Normal rank
@@ Property / cites work @@
+Certified Exact Transcendental Real Number Computation in Coq
+Normal rank
@@ Property / cites work @@
+Q4457464
@@ Property / cites work: Q4457464 / rank @@
+Normal rank
@@ Property / cites work @@
+Formalizing Bounded Increase
@@ Property / cites work: Formalizing Bounded Increase / rank @@
+Normal rank
@@ Property / cites work @@
+Toward a Lower Bound for Sorting Networks
@@ Property / cites work: Toward a Lower Bound for Sorting Networks / rank @@
+Normal rank