{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:06:13Z","timestamp":1784199973798,"version":"3.55.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\n                    <jats:bold>\n                      <jats:sc>Bean<\/jats:sc>\n                    <\/jats:bold>\n                    , a typed first-order programming language designed to express quantitative bounds on backward error.\n                    <jats:bold>\n                      <jats:sc>Bean<\/jats:sc>\n                    <\/jats:bold>\n                    \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\n                    <jats:bold>\n                      <jats:sc>Bean<\/jats:sc>\n                    <\/jats:bold>\n                    program denotes a triple of related transformations that together satisfy a backward error guarantee.\n                  <\/jats:p>\n                  <jats:p>\n                    To illustrate\n                    <jats:bold>\n                      <jats:sc>Bean<\/jats:sc>\n                    <\/jats:bold>\n                    \u2019s potential as a practical tool for automated backward error analysis, we implement a variety of standard algorithms from numerical linear algebra in\n                    <jats:bold>\n                      <jats:sc>Bean<\/jats:sc>\n                    <\/jats:bold>\n                    , 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\n                    <jats:bold>\n                      <jats:sc>Bean<\/jats:sc>\n                    <\/jats:bold>\n                    \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":3,"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"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-6516-1392","authenticated-orcid":false,"given":"Laura","family":"Zielinski","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8733-5799","authenticated-orcid":false,"given":"David","family":"Bindel","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"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"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/3636501.3636953"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1093\/imanum\/drad026"},{"key":"e_1_3_2_4_2","first-page":"121","volume-title":"Selected Papers from the 8th International Workshop on Computer Science Logic (CSL \u201994)","author":"Benton P. N.","year":"1994","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, Germany, 121\u2013135."},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328487"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1093\/imanum\/drl037"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_19"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1137\/20M1334796"},{"key":"e_1_3_2_9_2","doi-asserted-by":"crossref","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.","DOI":"10.1007\/978-1-4614-8453-0"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498692"},{"key":"e_1_3_2_12_2","first-page":"270","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018)","author":"Darulova Eva","year":"2018","unstructured":"Eva Darulova, Anastasiia Izycheva, Fariha Nasir, Fabian Ritter, Heiko Becker, and Robert Bastian. 2018. Daisy \u2013 Framework for Analysis and Optimization of Numerical Programs (Tool Paper). In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018). Dirk Beyer and Marieke Huisman (Eds.). Springer International Publishing, Cham, Switzerland, 270\u2013287."},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535874"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3014426"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.5555\/3433701.3433768"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/2746325.2746335"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2010.128"},{"key":"e_1_3_2_18_2","unstructured":"Valeria de Paiva. 1991. The Dialectica Categories. Ph.D. Dissertation. University of Cambridge Cambridge UK. Computer Laboratory Technical Report 213. https:\/\/www.cl.cam.ac.uk\/techreports\/UCAM-CL-TR-213.pdf"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/131766.131769"},{"key":"e_1_3_2_20_2","doi-asserted-by":"crossref","unstructured":"Peter Deuflhard and Andreas Hohmann. 2003. Numerical Analysis in Modern Scientific Computing: An Introduction (2nd ed.). Springer-Verlag Berlin Heidelberg Germany.","DOI":"10.1007\/978-0-387-21584-6"},{"key":"e_1_3_2_21_2","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 (2018). https:\/\/api.semanticscholar.org\/CorpusID:127679099"},{"key":"e_1_3_2_22_2","volume-title":"Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (Vancouver, Canada) (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 (Vancouver, Canada) (LICS \u201919). IEEE Press, USA, Article 11, 13 pages."},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/1232420.1232424"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814317"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429113"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951939"},{"issue":"4","key":"e_1_3_2_27_2","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 (Oct. 2012), 713\u2013726. https:\/\/www.cai.sk\/ojs\/index.php\/cai\/article\/view\/1101","journal-title":"COMPUTING AND INFORMATICS"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209165"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_18"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_3"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-8191(01)00141-7"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1137\/0613014"},{"key":"e_1_3_2_33_2","doi-asserted-by":"crossref","unstructured":"Nicholas J. Higham. 2002. Accuracy and Stability of Numerical Algorithms (2nd ed.). Society for Industrial and Applied Mathematics USA.","DOI":"10.1137\/1.9780898718027"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","unstructured":"Ariel Kellison Laura Zielinski David Bindel and Justin Hsu. 2025. Bean: A Language for Backward Error Analysis. doi:10.5281\/zenodo.15225350","DOI":"10.5281\/zenodo.15225350"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH58626.2023.00021"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656456"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/1089014.1089017"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3015465"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02450-5_12"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/356502.356497"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","unstructured":"Jean-Michel Muller Nicolas Brisebarre Florent de Dinechin Claude-Pierre Jeannerod Vincent Lef\u00e8vre Guillaume Melquiond Nathalie Revol Damien Stehl\u00e9 and Serge Torres. 2018. Handbook of Floating-Point Arithmetic (2nd ed.). Birkh\u00e4user Cham Cham Switzerland. doi:10.1007\/978-3-319-76526-6","DOI":"10.1007\/978-3-319-76526-6"},{"key":"e_1_3_2_42_2","unstructured":"NVIDIA. 2025. cuSolver Library. https:\/\/docs.nvidia.com\/cuda\/cusolver\/contents.html"},{"key":"e_1_3_2_43_2","unstructured":"U.S. Department of Energy. 2019. STRUMPACK: Structured Matrix Package. https:\/\/portal.nersc.gov\/project\/sparse\/strumpack\/"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","unstructured":"Dianne P. O\u2019Leary. 2009. Scientific Computing with Case Studies. Society for Industrial and Applied Mathematics Philadelphia PA USA. doi:10.1137\/9780898717723","DOI":"10.1137\/9780898717723"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1137\/0715024"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/3341714"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/3341714"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628160"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863568"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/2930660"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/3230733"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","unstructured":"Kasia \u015awirydowicz Eric Darve Wesley Jones Jonathan Maack Shaked Regev Michael A. Saunders Stephen J. Thomas and Slaven Pele\u0161. 2022. Linear solvers for power grid optimization problems: A review of GPU-accelerated linear solvers. Parallel Computing 111 (2022) 102870. doi:10.1016\/j.parco.2021.102870","DOI":"10.1016\/j.parco.2021.102870"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429074"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-73721-8_24"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","unstructured":"Lloyd N. Trefethen and David Bau. 1997. Numerical Linear Algebra. Society for Industrial and Applied Mathematics Philadelphia PA. doi:10.1137\/1.9780898719574","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":[[2026,7,16]],"date-time":"2026-07-16T10:07:08Z","timestamp":1784196428000},"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"}}]}}