Research talk: Correct computational law and civil procedure with the Lean Proof Assistant

Опубликовано 27 октября 2022, 15:40

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.

#MSFTResearchSummit

See related sessions in this track: microsoft.com/en-us/research/v...

Learn more about the 2022 Microsoft Research Summit: microsoft.com/en-us/research/e...