BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Jonathan Protzenko (Microsoft Research)
DTSTART:20221013T180000Z
DTEND:20221013T190000Z
DTSTAMP:20260423T035714Z
UID:OLS/103
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/OLS/103/">Co
 mputational Law: Programming Languages meet the Law</a>\nby Jonathan Protz
 enko (Microsoft Research) as part of Online logic seminar\n\n\nAbstract\nM
 any parts of the law\, such as tax code\, pension computations\, etc. enco
 de a clear and unambiguous algorithm: they are called computational law. B
 ut ordinary citizens without legal counsel are oftentimes powerless\, beca
 use layers of legalese and opaque implementations obscure the underlying a
 lgorithm.\n\nThe Correct Computational Law project tackles this inequity b
 y formalizing and capturing computational law using formal methods. Whethe
 r it is the French Tax Code\, French family benefits or Washington State's
  Legal Financial Obligations\, we formalize\, re-implement and find bugs i
 n 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.\n\nWe wi
 ll first describe our research agenda and ongoing efforts spanning France 
 and the US. Then\, we will focus on a case study: the complexity of federa
 l civil procedure in the US\, and how the Lean proof assistant can always 
 find\, with mathematical certainty\, a path through the pleading phase tha
 t fulfills all major procedural requirements.\n
LOCATION:https://researchseminars.org/talk/OLS/103/
END:VEVENT
END:VCALENDAR