1 files changed, 17 insertions, 0 deletions
diff --git a/src/riscv-spec.bib b/src/riscv-spec.bib
index 9f6d946..3d7157f 100644
--- a/src/riscv-spec.bib
+++ b/src/riscv-spec.bib
@@ -494,3 +494,20 @@ month =         {June},
 year =          {2010},
 address =       {Toronto, Canada}} 
 
+@article{roux:hal-01091186,
+  TITLE = {{Innocuous Double Rounding of Basic Arithmetic Operations}},
+  AUTHOR = {Roux, Pierre},
+  URL = {https://hal.archives-ouvertes.fr/hal-01091186},
+  JOURNAL = {{Journal of Formalized Reasoning}},
+  PUBLISHER = {{ASDD-AlmaDL}},
+  VOLUME = {7},
+  NUMBER = {1},
+  PAGES = {131-142},
+  YEAR = {2014},
+  MONTH = Nov,
+  DOI = {10.6092/issn.1972-5787/4359},
+  KEYWORDS = {Coq ; double rounding ; floating-point arithmetic},
+  PDF = {https://hal.archives-ouvertes.fr/hal-01091186/file/submission.pdf},
+  HAL_ID = {hal-01091186},
+  HAL_VERSION = {v1},
+}