Verified compilation of floating-point computations (Q2352505): Difference between revisions

@@ Property / describes a project that uses @@
+CompCert
@@ Property / describes a project that uses: CompCert / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W1988579293
@@ Property / OpenAlex ID: W1988579293 / rank @@
+Normal rank
@@ Property / cites work @@
+Multi-Prover Verification of Floating-Point Programs
+Normal rank
@@ Property / cites work @@
+Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd
+Normal rank
@@ Property / cites work @@
+Programming Languages and Systems
@@ Property / cites work: Programming Languages and Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic
+Normal rank
@@ Property / cites work @@
+A floating-point technique for extending the available precision
+Normal rank
@@ Property / cites work @@
+Q5674962
@@ Property / cites work: Q5674962 / rank @@
+Normal rank
@@ Property / cites work @@
+Handbook of Floating-Point Arithmetic
@@ Property / cites work: Handbook of Floating-Point Arithmetic / rank @@
+Normal rank
@@ Property / cites work @@
+Hardware-Dependent Proofs of Numerical Programs
@@ Property / cites work: Hardware-Dependent Proofs of Numerical Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Accurate Floating-Point Summation Part I: Faithful Rounding
+Normal rank
@@ Property / cites work @@
+A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7<sup>™</sup> Processor
+Normal rank