Research talk: Correct computational law and civil procedure with the Lean Proof Assistant
Computational law, such as tax law, or pension computations, encodes an algorithm. But in practice, the algorithm is hidden behind layers of legalese and obscure implementations, with no transparency or accountability.
The Correct Computational Law project applies formal methods to computational law. Whether it is French family benefits or Washington State’s Legal Financial Obligations, we formalize, re-implement and find bugs in the law. Doing so, we enable ordinary citizens to prevail over the complexity of the law, rather than falling prey to it.
First, we describe our research agenda spanning France and the US. Then, we study the complexity of US federal civil procedure, and how the Lean proof assistant can always find, with mathematical certainty, a path through the pleading phase that fulfills all major procedural requirements.
- Event:
- Research Summit 2022
- Track:
- Enabling a Resilient and Sustainable World
- Date:
-
-
Chris Bailey
JD Candidate
University of Illinois
-
Sharon Gillett
Technical Advisor and Sr. Principal Research Program Manager
-
Jonathan Protzenko
Principal Researcher
-
-