Microsoft Research Summit 2022 background tile pattern
Return to Event: Research Summit 2022

Research Summit 2022 • Videos

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.

Learn more about the 2022 Microsoft Research Summit >

Event:
Research Summit 2022
Track:
Enabling a Resilient and Sustainable World
Date:

Enabling a Resilient and Sustainable World