{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,18]],"date-time":"2026-10-18T07:03:03Z","timestamp":1792306983207,"version":"4.4.0"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T00:00:00Z","timestamp":1629331200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["683032"],"award-info":[{"award-number":["683032"]}],"id":[{"id":"10.13039\/501100000781","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":[[2021,8,22]]},"abstract":"<jats:p>Law at large underpins modern society, codifying and governing many aspects of citizens' daily lives. Oftentimes, law is subject to interpretation, debate and challenges throughout various courts and jurisdictions. But in some other areas, law leaves little room for interpretation, and essentially aims to rigorously describe a computation, a decision procedure or, simply said, an algorithm.<\/jats:p>\n          <jats:p>Unfortunately, prose remains a woefully inadequate tool for the job. The lack of formalism leaves room for ambiguities; the structure of legal statutes, with many paragraphs and sub-sections spread across multiple pages, makes it hard to compute the intended outcome of the algorithm underlying a given text; and, as with any other piece of poorly-specified critical software, the use of informal, natural language leaves corner cases unaddressed.<\/jats:p>\n          <jats:p>We introduce Catala, a new programming language that we specifically designed to allow a straightforward and systematic translation of statutory law into an executable implementation. Notably, Catala makes it natural and easy to express the general case \/ exceptions logic that permeates statutory law. Catala aims to bring together lawyers and programmers through a shared medium, which together they can understand, edit and evolve, bridging a gap that too often results in dramatically incorrect implementations of the law. We have implemented a compiler for Catala, and have proven the correctness of its core compilation steps using the F* proof assistant.<\/jats:p>\n          <jats:p>We evaluate Catala on several legal texts that are algorithms in disguise, notably section 121 of the US federal income tax and the byzantine French family benefits; in doing so, we uncover a bug in the official implementation of the French benefits. We observe as a consequence of the formalization process that using Catala enables rich interactions between lawyers and programmers, leading to a greater understanding of the original legislative intent, while producing a correct-by-construction executable specification reusable by the greater software ecosystem. Doing so, Catala increases trust in legal institutions, and mitigates the risk of societal damage due to incorrect implementations of the law.<\/jats:p>","DOI":"10.1145\/3473582","type":"journal-article","created":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T10:44:29Z","timestamp":1629369869000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":51,"title":["Catala: a programming language for the law"],"prefix":"10.1145","volume":"5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2247-0938","authenticated-orcid":false,"given":"Denis","family":"Merigoux","sequence":"first","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nicolas","family":"Chataing","sequence":"additional","affiliation":[{"name":"ENS, France \/ Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jonathan","family":"Protzenko","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,8,19]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009878"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.2307\/794073"},{"key":"e_1_2_2_3_1","unstructured":"Anne Broache. 2008. IRS trudges on with aging computers. https:\/\/www.cnet.com\/news\/irs-trudges-on-with-aging-computers\/  Anne Broache. 2008. IRS trudges on with aging computers. https:\/\/www.cnet.com\/news\/irs-trudges-on-with-aging-computers\/"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.3917\/tgs.035.0157"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-015-9383-0_3"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.3917\/tgs.035.0173"},{"key":"e_1_2_2_7_1","doi-asserted-by":"crossref","volume-title":"The Birth of Prolog","author":"Colmerauer Alain","DOI":"10.1145\/154766.155362"},{"key":"e_1_2_2_8_1","volume-title":"Designing a Generic Graph Library Using ML Functors.. Trends in functional programming, 8","author":"Conchon Sylvain","year":"2007"},{"key":"e_1_2_2_9_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"de Moura Leonardo"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.4775161"},{"key":"e_1_2_2_11_1","first-page":"17","article-title":"Logical method and law","volume":"10","author":"Dewey John","year":"1924","journal-title":"Cornell LQ"},{"key":"e_1_2_2_12_1","unstructured":"Derek Doran Sarah Schulz and Tarek R Besold. 2017. What does explainable AI really mean? A new conceptualization of perspectives. arXiv preprint arXiv:1710.00794.  Derek Doran Sarah Schulz and Tarek R Besold. 2017. What does explainable AI really mean? A new conceptualization of perspectives. arXiv preprint arXiv:1710.00794."},{"key":"e_1_2_2_13_1","unstructured":"Frank R. Konkel. 2018. The IRS system processing your taxes is almost 60 years old. https:\/\/www.nextgov.com\/it-modernization\/2018\/03\/irs-system-processing-your-taxes-almost-60-years-old\/146770\/  Frank R. Konkel. 2018. The IRS system processing your taxes is almost 60 years old. https:\/\/www.nextgov.com\/it-modernization\/2018\/03\/irs-system-processing-your-taxes-almost-60-years-old\/146770\/"},{"key":"e_1_2_2_14_1","unstructured":"Michael Genesereth. 2015. Computational Law. The Cop in the Backseat.  Michael Genesereth. 2015. Computational Law. The Cop in the Backseat."},{"key":"e_1_2_2_15_1","doi-asserted-by":"crossref","unstructured":"Randy Goebel Ajay Chander Katharina Holzinger Freddy Lecue Zeynep Akata Simone Stumpf Peter Kieseberg and Andreas Holzinger. 2018. Explainable ai: the new 42? In International cross-domain conference for machine learning and knowledge extraction. 295\u2013303.  Randy Goebel Ajay Chander Katharina Holzinger Freddy Lecue Zeynep Akata Simone Stumpf Peter Kieseberg and Andreas Holzinger. 2018. Explainable ai: the new 42? In International cross-domain conference for machine learning and knowledge extraction. 295\u2013303.","DOI":"10.1007\/978-3-319-99740-7_21"},{"key":"e_1_2_2_16_1","unstructured":"Government Accountability Office (GAO). 2021. COVID-19: Urgent Actions Needed to Better Ensure an Effective Federal Response \u2013 Report to Congressional Committees. https:\/\/www.gao.gov\/reports\/GAO-21-191\/##appendix24 Appendix 24 first table.  Government Accountability Office (GAO). 2021. COVID-19: Urgent Actions Needed to Better Ensure an Effective Federal Response \u2013 Report to Congressional Committees. https:\/\/www.gao.gov\/reports\/GAO-21-191\/##appendix24 Appendix 24 first table."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/COMPSAC.2018.00025"},{"key":"e_1_2_2_18_1","unstructured":"Nils Holzenberger Andrew Blair-Stanek and Benjamin Van Durme. 2020. A Dataset for Statutory Reasoning in Tax Law Entailment and Question Answering. arXiv preprint arXiv:2005.05257.  Nils Holzenberger Andrew Blair-Stanek and Benjamin Van Durme. 2020. A Dataset for Statutory Reasoning in Tax Law Entailment and Question Answering. arXiv preprint arXiv:2005.05257."},{"key":"e_1_2_2_20_1","unstructured":"Internal Revenue Service. [n.d.]. Exclusion of gain from sale of principal residence. https:\/\/www.law.cornell.edu\/uscode\/text\/26\/121  Internal Revenue Service. [n.d.]. Exclusion of gain from sale of principal residence. https:\/\/www.law.cornell.edu\/uscode\/text\/26\/121"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500618"},{"key":"e_1_2_2_22_1","article-title":"Literate","volume":"27","author":"Knuth D. E.","year":"1984","journal-title":"Programming. Comput. J."},{"key":"e_1_2_2_23_1","unstructured":"Sarah Lawsky. 2018. Formal Methods and the Law. https:\/\/popl18.sigplan.org\/details\/POPL-2018-papers\/3\/Formal-Methods-and-the-Law  Sarah Lawsky. 2018. Formal Methods and the Law. https:\/\/popl18.sigplan.org\/details\/POPL-2018-papers\/3\/Formal-Methods-and-the-Law"},{"key":"e_1_2_2_24_1","article-title":"Formalizing the Code","volume":"70","author":"Lawsky Sarah B.","year":"2017","journal-title":"Tax Law Review"},{"key":"e_1_2_2_25_1","doi-asserted-by":"crossref","unstructured":"Sarah B. Lawsky. 2018. A Logic for Statutes. Florida Tax Review.  Sarah B. Lawsky. 2018. A Logic for Statutes. Florida Tax Review.","DOI":"10.2139\/ssrn.3088206"},{"key":"e_1_2_2_26_1","unstructured":"Sarah B Lawsky. 2020. Form as Formalization. Ohio State Technology Law Journal.  Sarah B Lawsky. 2020. Form as Formalization. Ohio State Technology Law Journal."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1080\/13600869.2016.1232465"},{"key":"e_1_2_2_28_1","doi-asserted-by":"crossref","unstructured":"Rodolphe Lepigre and Christophe Raffalli. 2018. Abstract representation of binders in ocaml using the bindlib library. arXiv preprint arXiv:1807.01872.  Rodolphe Lepigre and Christophe Raffalli. 2018. Abstract representation of binders in ocaml using the bindlib library. arXiv preprint arXiv:1807.01872.","DOI":"10.4204\/EPTCS.274.4"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111320.1111042"},{"key":"e_1_2_2_30_1","unstructured":"Kif Leswing. 2020. New Jersey needs volunteers who know COBOL a 60-year-old programming language. https:\/\/www.cnbc.com\/2020\/04\/06\/new-jersey-seeks-cobol-programmers-to-fix-unemployment-system.html  Kif Leswing. 2020. New Jersey needs volunteers who know COBOL a 60-year-old programming language. https:\/\/www.cnbc.com\/2020\/04\/06\/new-jersey-seeks-cobol-programmers-to-fix-unemployment-system.html"},{"key":"e_1_2_2_31_1","volume-title":"Proof Automation with SMT, Tactics, and Metaprograms","author":"Mart\u00ednez Guido"},{"key":"e_1_2_2_32_1","doi-asserted-by":"crossref","unstructured":"Denis Merigoux Rapha\u00ebl Monat and Jonathan Protzenko. 2021. A Modern Compiler for the French Tax Code. Compiler Construction.  Denis Merigoux Rapha\u00ebl Monat and Jonathan Protzenko. 2021. A Modern Compiler for the French Tax Code. Compiler Construction.","DOI":"10.1145\/3446804.3446850"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237791"},{"key":"e_1_2_2_34_1","unstructured":"Antoine Min\u00e9 Xavier Leroy Pascal Cuoq and Christophe Troestler. 2011. The Zarith OCaml library. https:\/\/github.com\/ocaml\/Zarith  Antoine Min\u00e9 Xavier Leroy Pascal Cuoq and Christophe Troestler. 2011. The Zarith OCaml library. https:\/\/github.com\/ocaml\/Zarith"},{"key":"e_1_2_2_35_1","unstructured":"Jacques Monin. 2018. Louvois le logiciel qui a mis l\u2019arm\u00e9e \u00e0 terre. https:\/\/www.franceinter.fr\/emissions\/secrets-d-info\/secrets-d-info-27-janvier-2018  Jacques Monin. 2018. Louvois le logiciel qui a mis l\u2019arm\u00e9e \u00e0 terre. https:\/\/www.franceinter.fr\/emissions\/secrets-d-info\/secrets-d-info-27-janvier-2018"},{"key":"e_1_2_2_36_1","doi-asserted-by":"crossref","unstructured":"Jason Morris. 2020. Spreadsheets for Legal Reasoning: The Continued Promise of Declarative Logic Programming in Law. Available at SSRN 3577239.  Jason Morris. 2020. Spreadsheets for Legal Reasoning: The Continued Promise of Declarative Logic Programming in Law. Available at SSRN 3577239.","DOI":"10.2139\/ssrn.3577239"},{"key":"e_1_2_2_37_1","unstructured":"Marcos A Pertierra Sarah Lawsky Erik Hemberg and Una-May O\u2019Reilly. 2017. Towards Formalizing Statute Law as Default Logic through Automatic Semantic Parsing.. In ASAIL@ ICAIL.  Marcos A Pertierra Sarah Lawsky Erik Hemberg and Una-May O\u2019Reilly. 2017. Towards Formalizing Statute Law as Default Logic through Automatic Semantic Parsing.. In ASAIL@ ICAIL."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2892208.2892224"},{"key":"e_1_2_2_39_1","unstructured":"Fran\u00e7ois Pottier and Yann R\u00e9gis-Gianat. 2014. The Menhir Parser Generator. http:\/\/cambium.inria.fr\/~fpottier\/menhir\/  Fran\u00e7ois Pottier and Yann R\u00e9gis-Gianat. 2014. The Menhir Parser Generator. http:\/\/cambium.inria.fr\/~fpottier\/menhir\/"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34176-2_2"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(80)90014-4"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/CLOUD.2017.81"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/5689.5920"},{"key":"e_1_2_2_44_1","volume-title":"Un logiciel libre pour lutter contre l\u2019opacit\u00e9 du syst\u00e8me sociofiscal. Revue francaise de science politique, 69, 5","author":"Shulz S\u00e9bastien","year":"2019"},{"key":"e_1_2_2_45_1","unstructured":"Julien Signoles. 2011. The Calendar OCaml library. https:\/\/github.com\/ocaml-community\/calendar  Julien Signoles. 2011. The Calendar OCaml library. https:\/\/github.com\/ocaml-community\/calendar"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_2_47_1","unstructured":"Jonathan Turner. 2016. Shape of errors to come. https:\/\/blog.rust-lang.org\/2016\/08\/10\/Shape-of-errors-to-come.html  Jonathan Turner. 2016. Shape of errors to come. https:\/\/blog.rust-lang.org\/2016\/08\/10\/Shape-of-errors-to-come.html"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.2187"},{"key":"e_1_2_2_49_1","volume-title":"The Free Encyclopedia. https:\/\/en.wikipedia.org\/w\/index.php?title=Code_of_Ur-Nammu&oldid=998720276 [Online","author":"Wikipedia","year":"2021"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03592-1_13"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3473582","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3473582","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:28:16Z","timestamp":1750195696000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3473582"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,19]]},"references-count":49,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2021,8,22]]}},"alternative-id":["10.1145\/3473582"],"URL":"https:\/\/doi.org\/10.1145\/3473582","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,8,19]]},"assertion":[{"value":"2021-08-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}