Computational Law: Programming Languages meet the Law

Abstract: Many parts of the law, such as tax code, pension computations, etc. encode a clear and unambiguous algorithm: they are called computational law. But ordinary citizens without legal counsel are oftentimes powerless, because layers of legalese and opaque implementations obscure the underlying algorithm.

The Correct Computational Law project tackles this inequity by formalizing and capturing computational law using formal methods. Whether it is the French Tax Code, French family benefits or Washington State's Legal Financial Obligations, we formalize, re-implement and find bugs in the law. Doing so, we make it possible for ordinary citizens to prevail over the complexity of the law, rather than falling prey to it.

We will first describe our research agenda and ongoing efforts spanning France and the US. Then, we will focus on a case study: the complexity of federal civil procedure in the US, and how the Lean proof assistant can always find, with mathematical certainty, a path through the pleading phase that fulfills all major procedural requirements.

programming languagespublic financelogic

Audience: researchers in the topic

Online logic seminar

Series comments: Description: Seminar on all areas of logic