Formal proofs of rounding error bounds. With application to an automatic positive definiteness check (Q2013318): Difference between revisions

@@ 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 @@
+Canonical Big Operators
@@ Property / cites work: Canonical Big Operators / rank @@
+Normal rank
@@ Property / cites work @@
+Formal Proof of a Wave Equation Resolution Scheme: The Method Error
+Normal rank
@@ Property / cites work @@
+Construction of Real Algebraic Numbers in Coq
@@ Property / cites work: Construction of Real Algebraic Numbers in Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Q3024872
@@ Property / cites work: Q3024872 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4864704
@@ Property / cites work: Q4864704 / rank @@
+Normal rank
@@ Property / cites work @@
+Verification methods: Rigorous results using floating-point arithmetic
+Normal rank
@@ Property / cites work @@
+Verification of positive definiteness
@@ Property / cites work: Verification of positive definiteness / rank @@
+Normal rank
@@ Property / cites work @@
+Improved Backward Error Bounds for LU and Cholesky Factorizations
+Normal rank