ProLaLa 2023
who it's for
legal technologists, academic researchers, formal methods engineers, contract engineers, policy analysts, privacy engineers, programming language engineers
topics
Z3 SMT solver; first-order logic encoding; Answer Set Programming with constraints; Catala for legislation; DCR Graphs executable regulation; defeasible semantics for L4; Legistix consolidation DSL; Stipula live contract amendment; s-CASP relevance-driven semantics; privacy narrative generation; formalising criminal law in Catala
| title | author | length |
|---|---|---|
| Academic keynote : A Logician and Lawyer walk into a Classroom | Scott Shapiro, Ruzica Piskac | 50m |
Yale runs a Fall 2022 course "Law, Security, and Logic" that teaches first-order encoding and automated reasoning on real statutes; students formalize 50 USC… | ||
| Formal Modeling and Analysis of Legal Contracts using ContractCheck | Alan Khoja, Martin Kölbl, Stefan Leue, Rüdiger Wilhelmi | 23m |
ContractCheck encodes Sales Purchase Agreements as structured blocks and translates them into decidable fragments of first‑order logic (SMT2) checked by the Z3… | ||
| What do Relational Properties Have to Say About Legal Expert Systems ? | Arthur Correnson | 09m |
Legal expert systems often lack a formal single-input/specification so correctness is framed relationally by comparing runs; testing finds counterexamples but… | ||
| Building Information Modeling Using Constraint Logic Programming (Extended Ab... | Joaquín Arias, Seppo Törmä, Manuel Carro, Gopal Gupta | 24m |
Claims a unified BIM verifier that mixes geometric constraints and symbolic rules using CLP(Q/R) and an ASP-with-constraints engine, with a prototype 3D… | ||
| Exploring Consequences of Privacy Policies with Narrative Generation via Answ... | Chinmaya Dabral, Emma Tosch, Chris Martens | 11m |
A system encodes policy actors, roles and actions in Answer Set Programming to turn privacy clauses into constraints over a story planner, letting the model… | ||
| The Structure and Legal Interpretation of Computer Programs | James Grimmelmann | 28m |
Argues programs have three distinct legal meanings: naive functional meaning (what a particular execution actually does, e.g. an ATM debits but crashes)… | ||
| Deontic Paradoxes in Library Lending Regulations: A Case Study in Flint | Sterre Lutz | 09m |
Claims that Flint can encode Sergot’s library rules without producing the usual Chisholm-style contradiction. Formalization of the four library rules in Flint… | ||
| Defeasible Semantics for L4 | Guido Governatori, Meng Weng Wong | 09m |
An Answer Set Programming implementation provides defeasible semantics for L4 by compiling L4 rules (prescriptive, permissive, constitutive) into a… | ||
| Experience report: implementing a real-world, medium-sized program derived fr... | Denis Merigoux | 28m |
Replication of the French housing benefits system CRISTAL from CNAF laws uses Catala to reimplement about 7,000 lines of code and 100 pages of regulations… | ||
| Legal Contracts Amending in Stipula | Cosimo Laneve, Alessandro Parenti, Giovanni Sartor | 21m |
Extends Stipula with higher-order Stipula so contracts can receive live code updates, models two concrete amendment patterns: an additive amendment that… | ||
| Towards an Automatic Consolidation of French Law | Georges-André Silber | 22m |
A tool called Legistix converts Official Journal patch texts into executable consolidation programs by combining layered regex/compound grammars with a new… | ||
| DCR Graphs as Co-created Executable Models of the Law | Thomas T. Hildebrandt | 13m |
A formal declarative language developed over 15 years for executable models of regulation, claiming maintainable encoding of decision rules and temporal… | ||
| Visual Propositional Logic With yscript | William O'Hanley | 14m |
yscript programs render as a live boxes-and-wires graph derived from source so edits update the view, with a VS Code extension using tree-sitter to map nodes… | ||
| Research keynote | Chris Bailey | 42m |
Formalizes the pleading stage by encoding Federal Rules into Lean, shipping a date and time library in Lean and an implemented algorithm for Rule 6 that… | ||
| Designing an experiment for comparing user interfaces for legal formalization | Tereza Novotna, Tomer Libal | 21m |
A prototype normative AI tool annotates legal text segments and maps them to formal logical relations; the claim is that four measurable qualities —… | ||
| Blawx: User-friendly Goal-Directed Answer Set Programming for Rules as Code | Jason Morris | 13m |
Blawx is a web prototype that encodes statutes into goal-directed answer set programs using goal-directed ASP and a block-based UI, implemented with Blockly +… | ||
| Formalising Criminal Law in Catala | Luca Arnaboldi, David Aspinall, Ronny Bogani, Burkhard Schafer, Scott Herman, Jonathan Protzenko, Ekaterina Komendantskaya, Remi Desmartin, Yue Li | 20m |
Formalisation uses the Catala DSL to implement a DUI fine calculator for Florida law that inputs blood alcohol, prior DUI dates and damage and outputs min/max… | ||
| nothing matches | ||