{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,27]],"date-time":"2026-03-27T17:12:10Z","timestamp":1774631530056,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":55,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,1]]},"DOI":"10.1145\/3009837.3009846","type":"proceedings-article","created":{"date-parts":[[2016,12,22]],"date-time":"2016-12-22T16:20:29Z","timestamp":1482423629000},"page":"300-315","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":92,"title":["Rigorous floating-point mixed-precision tuning"],"prefix":"10.1145","author":[{"given":"Wei-Fan","family":"Chiang","sequence":"first","affiliation":[{"name":"University of Utah, USA"}]},{"given":"Mark","family":"Baranowski","sequence":"additional","affiliation":[{"name":"University of Utah, USA"}]},{"given":"Ian","family":"Briggs","sequence":"additional","affiliation":[{"name":"University of Utah, USA"}]},{"given":"Alexey","family":"Solovyev","sequence":"additional","affiliation":[{"name":"University of Utah, USA"}]},{"given":"Ganesh","family":"Gopalakrishnan","sequence":"additional","affiliation":[{"name":"University of Utah, USA"}]},{"given":"Zvonimir","family":"Rakamari\u0107","sequence":"additional","affiliation":[{"name":"University of Utah, USA"}]}],"member":"320","published-online":{"date-parts":[[2017,1]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/3007337.3007352"},{"key":"e_1_3_2_1_2_1","volume-title":"ARM NEON general-purpose SIMD engine","author":"ARM","year":"2016","unstructured":"ARM NEON. ARM NEON general-purpose SIMD engine , 2016 . ARM NEON. ARM NEON general-purpose SIMD engine, 2016."},{"key":"e_1_3_2_1_3_1","volume-title":"High-precision arithmetic: Progress and challenges","author":"Bailey D.","year":"2013","unstructured":"D. Bailey and J. Borwein . High-precision arithmetic: Progress and challenges , 2013 . D. Bailey and J. Borwein. High-precision arithmetic: Progress and challenges, 2013."},{"key":"e_1_3_2_1_4_1","volume-title":"Universit\u00e9 Paris-Sud","author":"Boldo S.","year":"2014","unstructured":"S. Boldo . Deductive Formal Verification: How To Make Your Floating-Point Programs Behave. Th\u00e8se d\u2019habilitation , Universit\u00e9 Paris-Sud , 2014 . S. Boldo. Deductive Formal Verification: How To Make Your Floating-Point Programs Behave. Th\u00e8se d\u2019habilitation, Universit\u00e9 Paris-Sud, 2014."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-014-9317-x"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-013-0203-7"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH.2015.26"},{"key":"e_1_3_2_1_8_1","first-page":"76","volume-title":"Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design (FMCAD)","author":"Brillout A.","year":"2009","unstructured":"A. Brillout , D. Kroening , and T. Wahl . Mixed abstractions for floatingpoint arithmetic . In Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design (FMCAD) , pages 69\u2013 76 , 2009 . A. Brillout, D. Kroening, and T. Wahl. Mixed abstractions for floatingpoint arithmetic. In Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design (FMCAD), pages 69\u201376, 2009."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2576779.2576783"},{"key":"e_1_3_2_1_10_1","volume-title":"High Performance Computing and Grids in Action","author":"Buttari A.","year":"2008","unstructured":"A. Buttari , J. Dongarra , J. Kurzak , J. Langou , J. Langou , P. Luszczek , and S. Tomov . Exploiting mixed precision floating point hardware in scientific computations . In High Performance Computing and Grids in Action . IOS Press , 2008 . A. Buttari, J. Dongarra, J. Kurzak, J. Langou, J. Langou, P. Luszczek, and S. Tomov. Exploiting mixed precision floating point hardware in scientific computations. In High Performance Computing and Grids in Action. IOS Press, 2008."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1377596.1377597"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1654059.1654065"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535858"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2555243.2555265"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-29778-1_17"},{"key":"e_1_3_2_1_16_1","volume-title":"The Coq proof assistant","year":"2016","unstructured":"Coq. The Coq proof assistant , 2016 . Coq. The Coq proof assistant, 2016."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048094"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535874"},{"key":"e_1_3_2_1_19_1","volume-title":"Towards a compiler for reals. CoRR, abs\/1410.0198","author":"Darulova E.","year":"2016","unstructured":"E. Darulova and V. Kuncak . Towards a compiler for reals. CoRR, abs\/1410.0198 , 2016 . E. Darulova and V. Kuncak. Towards a compiler for reals. CoRR, abs\/1410.0198, 2016."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/2555754.2555776"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1141277.1141584"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_14"},{"key":"e_1_3_2_1_23_1","volume-title":"not just another interval library","year":"2016","unstructured":"Gaol. Gaol , not just another interval library ., 2016 . Gaol. Gaol, not just another interval library., 2016."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/103162.103163"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2493882"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_3"},{"key":"e_1_3_2_1_27_1","volume-title":"17th International Symposium on Scientific Computing, Computer Arithmetics and Verified Numerics (SCAN)","author":"Graillat S.","year":"2016","unstructured":"S. Graillat , F. J\u00e9z\u00e9quel , R. Picot , F. F\u00e9votte , and B. Lathuili\u00e9re . PROMISE : floating-point precision tuning with stochastic arithmetic . In 17th International Symposium on Scientific Computing, Computer Arithmetics and Verified Numerics (SCAN) , 2016 . S. Graillat, F. J\u00e9z\u00e9quel, R. Picot, F. F\u00e9votte, and B. Lathuili\u00e9re. PROMISE : floating-point precision tuning with stochastic arithmetic. In 17th International Symposium on Scientific Computing, Computer Arithmetics and Verified Numerics (SCAN), 2016."},{"key":"e_1_3_2_1_28_1","volume-title":"Gurobi optimizer","year":"2016","unstructured":"Gurobi. Gurobi optimizer , 2016 . Gurobi. Gurobi optimizer, 2016."},{"key":"e_1_3_2_1_29_1","volume-title":"The End of Error: Unum Computing","author":"Gustafson J. L.","year":"2015","unstructured":"J. L. Gustafson . The End of Error: Unum Computing . Chapman and Hall\/CRC , 2015 . J. L. Gustafson. The End of Error: Unum Computing. Chapman and Hall\/CRC, 2015."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/11757283_8"},{"key":"e_1_3_2_1_31_1","volume-title":"The HOL Light theorem prover","author":"Light HOL","year":"2016","unstructured":"HOL Light . The HOL Light theorem prover , 2016 . HOL Light. The HOL Light theorem prover, 2016."},{"key":"e_1_3_2_1_32_1","volume-title":"IEEE standard for floating-point arithmetic","author":"IEEE","year":"2008","unstructured":"IEEE 754. IEEE standard for floating-point arithmetic , 2008 . IEEE 754. IEEE standard for floating-point arithmetic, 2008."},{"key":"e_1_3_2_1_33_1","volume-title":"Intel intrinsics guide","year":"2016","unstructured":"Intel Intrinsics for Type Casting. Intel intrinsics guide , 2016 . Intel Intrinsics for Type Casting. Intel intrinsics guide, 2016."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.10.010"},{"key":"e_1_3_2_1_35_1","volume-title":"How futile are mindless assessments of roundoff in floating-point computation?","author":"Kahan W.","year":"2006","unstructured":"W. Kahan . How futile are mindless assessments of roundoff in floating-point computation? , 2006 . W. Kahan. How futile are mindless assessments of roundoff in floating-point computation?, 2006."},{"key":"e_1_3_2_1_36_1","first-page":"518","volume-title":"Proceedings of the 17th International Conference on Machine Learning (ICML)","author":"Lagoudakis M.","year":"2000","unstructured":"M. Lagoudakis and M. Littman . Algorithm selection using reinforcement learning . In Proceedings of the 17th International Conference on Machine Learning (ICML) , pages 511\u2013 518 , 2000 . M. Lagoudakis and M. Littman. Algorithm selection using reinforcement learning. In Proceedings of the 17th International Conference on Machine Learning (ICML), pages 511\u2013518, 2000."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2464996.2465018"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908107"},{"key":"e_1_3_2_1_39_1","first-page":"4","volume-title":"Proceedings of the Conference on Design, Automation & Test in Europe (DATE)","author":"Leeser M.","year":"2014","unstructured":"M. Leeser , S. Mukherjee , J. Ramachandran , and T. Wahl . Make it real: Effective floating-point reasoning via exact arithmetic . In Proceedings of the Conference on Design, Automation & Test in Europe (DATE) , pages 117:1\u2013117: 4 , 2014 . M. Leeser, S. Mukherjee, J. Ramachandran, and T. Wahl. Make it real: Effective floating-point reasoning via exact arithmetic. In Proceedings of the Conference on Design, Automation & Test in Europe (DATE), pages 117:1\u2013117:4, 2014."},{"key":"e_1_3_2_1_40_1","volume-title":"The GCC quad-precision math library","year":"2016","unstructured":"lquadmath. The GCC quad-precision math library , 2016 . lquadmath. The GCC quad-precision math library, 2016."},{"key":"e_1_3_2_1_41_1","volume-title":"Certified roundoff error bounds using semidefinite programming. CoRR, abs\/1507.03331","author":"Magron V.","year":"2015","unstructured":"V. Magron , G. A. Constantinides , and A. F. Donaldson . Certified roundoff error bounds using semidefinite programming. CoRR, abs\/1507.03331 , 2015 . V. Magron, G. A. Constantinides, and A. F. Donaldson. Certified roundoff error bounds using semidefinite programming. CoRR, abs\/1507.03331, 2015."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480945.1480960"},{"key":"e_1_3_2_1_43_1","volume-title":"Nvidia tweaks Pascal GPU for deep learning push","author":"Morgan T. P.","year":"2015","unstructured":"T. P. Morgan . Nvidia tweaks Pascal GPU for deep learning push , 2015 . T. P. Morgan. Nvidia tweaks Pascal GPU for deep learning push, 2015."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2014.59"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737959"},{"key":"e_1_3_2_1_46_1","unstructured":"QCQP. Quadratically constrained quadratic program 2016.  QCQP. Quadratically constrained quadratic program 2016."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2503210.2503296"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884850"},{"key":"e_1_3_2_1_49_1","volume-title":"Informal Proceedings of 8th International Workshop on Satisfiability Modulo Theories (SMT)","author":"R\u00fcmmer P.","year":"2010","unstructured":"P. R\u00fcmmer and T. Wahl . An SMT-LIB theory of binary floating-point arithmetic . In Informal Proceedings of 8th International Workshop on Satisfiability Modulo Theories (SMT) , 2010 . P. R\u00fcmmer and T. Wahl. An SMT-LIB theory of binary floating-point arithmetic. In Informal Proceedings of 8th International Workshop on Satisfiability Modulo Theories (SMT), 2010."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594302"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/PL00009321"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19249-9_33"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1831708.1831724"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1177\/1094342004041293"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.5555\/2818754.2818820"}],"event":{"name":"POPL '17: The 44th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","location":"Paris France","acronym":"POPL '17","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009846","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3009837.3009846","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:36:21Z","timestamp":1750203381000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009846"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1]]},"references-count":55,"alternative-id":["10.1145\/3009837.3009846","10.1145\/3009837"],"URL":"https:\/\/doi.org\/10.1145\/3009837.3009846","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3093333.3009846","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2017,1]]},"assertion":[{"value":"2017-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}