{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:34:08Z","timestamp":1767929648969,"version":"3.49.0"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T00:00:00Z","timestamp":1749772800000},"content-version":"vor","delay-in-days":3,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,6,10]]},"abstract":"<jats:p>\n            <jats:italic toggle=\"yes\">Backward error analysis<\/jats:italic>\n            offers a method for assessing the quality of numerical programs in the presence of floating-point rounding errors. However, techniques from the numerical analysis literature for quantifying backward error require substantial human effort, and there are currently no tools or automated methods for statically deriving sound backward error bounds. To address this gap, we propose Bean, a typed first-order programming language designed to express quantitative bounds on backward error. Bean\u2019s type system combines a graded coeffect system with strict linearity to soundly track the flow of backward error through programs. We prove the soundness of our system using a novel categorical semantics, where every Bean program denotes a triple of related transformations that together satisfy a backward error guarantee.\n          <\/jats:p>\n          <jats:p>\n            To illustrate Bean\u2019s potential as a practical tool for automated backward error analysis, we implement a variety of standard algorithms from numerical linear algebra in Bean, establishing fine-grained backward error bounds via typing in a compositional style. We also develop a prototype implementation of Bean that infers backward error bounds automatically. Our evaluation shows that these inferred bounds match worst-case theoretical relative backward error bounds from the literature, underscoring Bean\u2019s utility in validating a key property of numerical programs:\n            <jats:italic toggle=\"yes\">numerical stability<\/jats:italic>\n            .\n          <\/jats:p>","DOI":"10.1145\/3729324","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"1838-1862","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Bean: A Language for Backward Error Analysis"],"prefix":"10.1145","volume":"9","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\/0009-0006-6516-1392","authenticated-orcid":false,"given":"Laura","family":"Zielinski","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8733-5799","authenticated-orcid":false,"given":"David","family":"Bindel","sequence":"additional","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"},{"name":"Imperial College London, London, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3636501.3636953"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1093\/imanum\/drad026"},{"key":"e_1_2_2_3_1","volume-title":"Selected Papers from the 8th International Workshop on Computer Science Logic (CSL \u201994)","author":"Benton P. N.","unstructured":"P. N. Benton. 1994. A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models (Extended Abstract). In Selected Papers from the 8th International Workshop on Computer Science Logic (CSL \u201994). Springer-Verlag, Berlin, Heidelberg. 121\u2013135. isbn:3540600175"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328487"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1093\/imanum\/drl037"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_19"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1137\/20M1334796"},{"key":"e_1_2_2_8_1","volume-title":"Corless and Nicolas Fillion","author":"Robert","year":"2013","unstructured":"Robert M. Corless and Nicolas Fillion. 2013. A Graduate Introduction to Numerical Methods: From the Viewpoint of Backward Error Analysis. Springer Publishing Company, Incorporated, USA. isbn:1461484529"},{"key":"e_1_2_2_9_1","volume-title":"The ASTRE\u00c9 Analyzer","author":"Cousot Patrick","year":"1987","unstructured":"Patrick Cousot, Radhia Cousot, Jer\u00f4me Feret, Laurent Mauborgne, Antoine Min\u00e9, David Monniaux, and Xavier Rival. 2005. The ASTRE\u00c9 Analyzer. In Programming Languages and Systems, Mooly Sagiv (Ed.) (ESOP 2005). Springer Berlin Heidelberg, Berlin, Heidelberg. 21\u201330. isbn:978-3-540-31987-0"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498692"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_15"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535874"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3014426"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/3433701.3433768"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2746325.2746335"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2010.128"},{"key":"e_1_2_2_17_1","volume-title":"The Dialectica Categories. Ph. D. Dissertation","author":"de Paiva Valeria","unstructured":"Valeria de Paiva. 1991. The Dialectica Categories. Ph. D. Dissertation. University of Cambridge. https:\/\/www.cl.cam.ac.uk\/techreports\/UCAM-CL-TR-213.pdf Computer Laboratory Technical Report 213"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/131766.131769"},{"key":"e_1_2_2_19_1","volume-title":"Numerical Analysis in Modern Scientific Computing: An Introduction (2 ed.)","author":"Deuflhard Peter","unstructured":"Peter Deuflhard and Andreas Hohmann. 2003. Numerical Analysis in Modern Scientific Computing: An Introduction (2 ed.). Springer-Verlag, Berlin, Heidelberg. isbn:0387954104"},{"key":"e_1_2_2_20_1","unstructured":"Iain S. Duff Jd Hogg and Florent Lopez. 2018. A new sparse symmetric indefinite solver using a posteriori threshold pivoting. Rutherford Appleton Laboratory Technical Reports https:\/\/api.semanticscholar.org\/CorpusID:127679099"},{"key":"e_1_2_2_21_1","volume-title":"Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201919)","author":"Fong Brendan","year":"2021","unstructured":"Brendan Fong, David Spivak, and R\u00e9my Tuy\u00e9ras. 2021. Backprop as functor: a compositional perspective on supervised learning. In Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201919). IEEE Press, USA. Article 11, 13 pages."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1232420.1232424"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814317"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429113"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951939"},{"key":"e_1_2_2_26_1","first-page":"713","article-title":"Miller Analyzer for Matlab: A Matlab Package for Automatic Roundoff Analysis","volume":"31","author":"G\u00e1ti Attila","year":"2012","unstructured":"Attila G\u00e1ti. 2012. Miller Analyzer for Matlab: A Matlab Package for Automatic Roundoff Analysis. COMPUTING AND INFORMATICS, 31, 4 (2012), Oct., 713\u2013726. https:\/\/www.cai.sk\/ojs\/index.php\/cai\/article\/view\/1101","journal-title":"COMPUTING AND INFORMATICS"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209165"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_18"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_3"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-8191(01)00141-7"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1137\/0613014"},{"key":"e_1_2_2_32_1","volume-title":"Accuracy and Stability of Numerical Algorithms (2 ed.)","author":"Higham Nicholas J.","unstructured":"Nicholas J. Higham. 2002. Accuracy and Stability of Numerical Algorithms (2 ed.). Society for Industrial and Applied Mathematics, USA. isbn:0898715210"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.15225350"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH58626.2023.00021"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656456"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1089014.1089017"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3015465"},{"key":"e_1_2_2_38_1","volume-title":"Strongly Typed Numerical Computations","author":"Martel Matthieu","unstructured":"Matthieu Martel. 2018. Strongly Typed Numerical Computations. In Formal Methods and Software Engineering, Jing Sun and Meng Sun (Eds.). Springer International Publishing, Cham. 197\u2013214. isbn:978-3-030-02450-5"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/356502.356497"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-76526-6"},{"key":"e_1_2_2_41_1","unstructured":"NVIDIA. 2025. cuSolver Library. https:\/\/docs.nvidia.com\/cuda\/cusolver\/contents.html"},{"key":"e_1_2_2_42_1","volume-title":"STRUMPACK: Structured Matrix Package. https:\/\/portal.nersc.gov\/project\/sparse\/strumpack\/","author":"U.S. Department of Energy.","year":"2019","unstructured":"U.S. Department of Energy. 2019. STRUMPACK: Structured Matrix Package. https:\/\/portal.nersc.gov\/project\/sparse\/strumpack\/"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1137\/9780898717723"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1137\/0715024"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341714"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341714"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628160"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863568"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2930660"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230733"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.parco.2021.102870"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429074"},{"key":"e_1_2_2_53_1","volume-title":"Mu\u00f1oz","author":"Titolo Laura","year":"2018","unstructured":"Laura Titolo, Marco A. Feli\u00fa, Mariano Moscato, and C\u00e9sar A. Mu\u00f1oz. 2018. An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs. In Verification, Model Checking, and Abstract Interpretation, Isil Dillig and Jens Palsberg (Eds.). Springer International Publishing, Cham. 516\u2013537. isbn:978-3-319-73721-8"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898719574"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729324","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729324","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,16]],"date-time":"2025-07-16T06:07:00Z","timestamp":1752646020000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729324"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":54,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729324"],"URL":"https:\/\/doi.org\/10.1145\/3729324","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}