{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:11:48Z","timestamp":1775790708167,"version":"3.50.1"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["943130"],"award-info":[{"award-number":["943130"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000015","name":"U.S. Department of Energy","doi-asserted-by":"publisher","award":["DE-SC0021110"],"award-info":[{"award-number":["DE-SC0021110"]}],"id":[{"id":"10.13039\/100000015","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-23-1-2134"],"award-info":[{"award-number":["N00014-23-1-2134"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,6,20]]},"abstract":"<jats:p>\n            Algorithms operating on real numbers are implemented as floating-point computations in practice, but floatingpoint operations introduce\n            <jats:italic toggle=\"yes\">roundoff errors<\/jats:italic>\n            that can degrade the accuracy of the result. We propose\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\" overflow=\"scroll\">\n                <mml:msub>\n                  <mml:mi mathvariant=\"normal\">\u039b<\/mml:mi>\n                  <mml:mi fontfamily=\"Georgia\" mathvariant=\"bold\">num<\/mml:mi>\n                <\/mml:msub>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            , a functional programming language with a type system that can express quantitative bounds on roundoff error. Our type system combines a sensitivity analysis, enforced through a linear typing discipline, with a novel graded monad to track the accumulation of roundoff errors. We prove that our type system is sound by relating the denotational semantics of our language to the exact and floating-point operational semantics.\n          <\/jats:p>\n          <jats:p>\n            To demonstrate our system, we instantiate\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\" overflow=\"scroll\">\n                <mml:msub>\n                  <mml:mi mathvariant=\"normal\">\u039b<\/mml:mi>\n                  <mml:mi fontfamily=\"Georgia\" mathvariant=\"bold\">num<\/mml:mi>\n                <\/mml:msub>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            with error metrics proposed in the numerical analysis literature and we show how to incorporate rounding operations that faithfully model aspects of the IEEE 754 floating-point standard. To show that\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\" overflow=\"scroll\">\n                <mml:msub>\n                  <mml:mi mathvariant=\"normal\">\u039b<\/mml:mi>\n                  <mml:mi fontfamily=\"Georgia\" mathvariant=\"bold\">num<\/mml:mi>\n                <\/mml:msub>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            can be a useful tool for automated error analysis, we develop a prototype implementation for\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\" overflow=\"scroll\">\n                <mml:msub>\n                  <mml:mi mathvariant=\"normal\">\u039b<\/mml:mi>\n                  <mml:mi fontfamily=\"Georgia\" mathvariant=\"bold\">num<\/mml:mi>\n                <\/mml:msub>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            that infers error bounds that are competitive with existing tools, while often running significantly faster. Finally, we consider semantic extensions of our graded monad to bound error under more complex rounding behaviors, such as non-deterministic and randomized rounding.\n          <\/jats:p>","DOI":"10.1145\/3656456","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"1954-1978","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Numerical Fuzz: A Type System for Rounding Error Analysis"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3177-7958","authenticated-orcid":false,"given":"Ariel E.","family":"Kellison","sequence":"first","affiliation":[{"name":"Cornell University, Ithaca, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8953-7060","authenticated-orcid":false,"given":"Justin","family":"Hsu","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-44245-2_4"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3636501.3636953"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.5555\/2060081"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/2746325.2746335"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009890"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785715"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.CAMWA.2014.06.004"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","unstructured":"Sylvie Boldo Claude-Pierre Jeannerod Guillaume Melquiond and Jean-Michel Muller. 2023. Floating-point arithmetic. Acta Numerica 32 (2023) 203\u2013290. https:\/\/doi.org\/10.1017\/S0962492922000101 10.1017\/S0962492922000101","DOI":"10.1017\/S0962492922000101"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH.2011.40"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_19"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89330-1_2"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1137\/20M1334796"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","unstructured":"Germund Dahlquist and \u00c5ke Bj\u00f6rck. 2008. Numerical Methods in Scientific Computing Volume I. Society for Industrial and Applied Mathematics. https:\/\/doi.org\/10.1137\/1.9780898717785 10.1137\/1.9780898717785","DOI":"10.1137\/1.9780898717785"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","unstructured":"Ugo Dal Lago and Francesco Gavazzo. 2022. A Relational Theory of Effects and Coeffects. 6 POPL Article 31 (Jan. 2022). https:\/\/doi.org\/10.1145\/3498692 10.1145\/3498692","DOI":"10.1145\/3498692"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-54292-8_6"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_15"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535874"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3014426"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","unstructured":"Arnab Das Ian Briggs Ganesh Gopalakrishnan Sriram Krishnamoorthy and Pavel Panchekha. 2020. Scalable yet Rigorous Floating-Point Error Analysis. In International Conference for High Performance Computing Networking Storage and Analysis (SC20). 1\u201314. https:\/\/doi.org\/10.1109\/SC41405.2020.00055 10.1109\/SC41405.2020.00055","DOI":"10.1109\/SC41405.2020.00055"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/1644001.1644003"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49630-5_30"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429113"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951939"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90386-T"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/103162.103163"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_3"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0000475"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48256-3_9"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-40922-X_14"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","unstructured":"Nicholas J. Higham. 2002. Accuracy and Stability of Numerical Algorithms (2nd ed.). Society for Industrial and Applied Mathematics. https:\/\/doi.org\/10.1137\/1.9780898718027 10.1137\/1.9780898718027 arXiv:https:\/\/doi.org\/10.1137\/1.9780898718027 10.1137\/1.9780898718027 arXiv:https:\/\/epubs.siam.org\/doi\/pdf\/10.1137\/1.9780898718027 10.1137\/1.9780898718027","DOI":"10.1137\/1.9780898718027"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1137\/18M1226312"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535846"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-21222-2_9"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH58626.2023.00021"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","unstructured":"Ariel E. Kellison and Justin Hsu. 2024. Numerical Fuzz: A Type System for Rounding Error Analysis. https:\/\/doi.org\/10.5281\/zenodo.10802849 10.5281\/zenodo.10802849","DOI":"10.5281\/zenodo.10802849"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107360068"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498664"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/3015465"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02450-5_12"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1474-6670(17)44820-8"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30942-8_3"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1137\/0715024"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","unstructured":"Pavel Panchekha Alex Sanchez-Stern James R. Wilcox and Zachary Tatlock. 2015. Automatically improving accuracy for floating point expressions. (2015) 1\u201311. https:\/\/doi.org\/10.1145\/2737924.2737959 10.1145\/2737924.2737959","DOI":"10.1145\/2737924.2737959"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854066"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","unstructured":"Jason Reed and Benjamin C. Pierce. 2010. Distance makes the types grow stronger: a calculus for differential privacy. (2010) 157\u2013168. https:\/\/doi.org\/10.1145\/1863543.1863568 10.1145\/1863543.1863568","DOI":"10.1145\/1863543.1863568"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","unstructured":"Eric Schkufza Rahul Sharma and Alex Aiken. 2014. Stochastic optimization of floating-point programs with tunable precision. (2014) 53\u201364. https:\/\/doi.org\/10.1145\/2594291.2594302 10.1145\/2594291.2594302","DOI":"10.1145\/2594291.2594302"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/3230733"},{"key":"e_1_3_1_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-42753-4_14"},{"key":"e_1_3_1_52_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-73721-8_24"},{"key":"e_1_3_1_53_2","unstructured":"Lei Yu. 2013. A Formal Model of IEEE Floating Point Arithmetic. Archive of Formal Proofs (July 2013). https:\/\/isaafp.org\/entries\/IEEE_Floating_Point.html Formal proof development."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656456","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656456","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:42:31Z","timestamp":1751661751000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656456"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":52,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656456"],"URL":"https:\/\/doi.org\/10.1145\/3656456","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}