Sun 15 Jan 2023 09:10 - 09:55 at Kenmore - Session #1 Chair(s): Shrutarshi Basu, Jonathan Protzenko

While researchers are becoming to appreciate the natural connections between law and computer science, the number of courses where students can learn about logic, law, and automated reasoning are few. Even Yale University, which is traditionally oriented towards humanities- and law-related disciplines, has never had such a course. In Fall 2022 semester, Professor Piskac (Yale CS Department) and Professor Shapiro (Yale Law School) jointly taught "Law, Security, and Logic” for the first time. The student body was diverse, both in terms of their declared majors, as well as race and gender. Few students had encountered techniques of automated reasoning or legal reasoning.

This talk will report on our experiences in teaching this course. The course was a combination of traditional lectures and application-type work. The course instructors gave lectures covering the basic themes, such as first-order logic, automated reasoning, SMT solvers, legal reasoning, and legal interpretation. The students also got hands-on experience: they used existing automated reasoning tools to model real-world protocols and show their correctness or detect vulnerabilities.

Moreover, students used automated reasoning tools to check regulatory compliance automatically. There are many statutes and regulations that are a challenge to understand, even for experts. The Foreign Intelligence Surveillance Act of 1978 (FISA) is a prime example. FISA is the main authorization for foreign intelligence collection in the United States. It is an extremely important statute and our students were intensely interested in it, as it regulates domestic surveillance of the internet. Unfortunately, FISA is an extremely complicated statute. Evidence even suggests that it was intentionally drafted to obfuscate its meaning. Entire courses in law school are devoted to it. In the class, the students used first-order logic to formulate the definition of electronic surveillance as set out in 50 USC 1801(f). They automatically checked various scenarios to determine whether they would be considered “electronic surveillance” under FISA.

Based on this class, we believe that formal automated reasoning can be applied to legal topics, such as formalizing norms used in privacy policy regulations, legal rental contracts, or property law, just to name a few, which are the standard topics considered in this workshop, and can be taught to undergraduate CS majors.

We will conclude this talk with suggestions about additional research directions that combine legal and automated reasoning. In particular, we will describe our ongoing project on using counterfactual reasoning for legal accountability, as well as using formal methods to exploit legal code.

Sun 15 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:30
Session #1ProLaLa at Kenmore
Chair(s): Shrutarshi Basu Harvard University, Jonathan Protzenko Microsoft Research, Redmond
Day opening
Opening comments
Jonathan Protzenko Microsoft Research, Redmond, Denis Merigoux INRIA, Shrutarshi Basu Middlebury College
Academic keynote : A Logician and Lawyer walk into a Classroom
Scott Shapiro Yale Law School, Ruzica Piskac Yale University
Formal Modeling and Analysis of Legal Contracts using ContractCheck
Alan Khoja University of Konstanz, Martin Kölbl CertiK, Stefan Leue University of Konstanz, Rüdiger Wilhelmi University of Konstanz
DOI Pre-print
What do Relational Properties Have to Say About Legal Expert Systems ?
Arthur Correnson École Normale Supérieure de Rennes & Saarland University