Legal Calculi
summary
Proposes a concrete middle layer: small, domain-specific legal calculi that compile nontrivially from human-facing DSLs (Orlando for property, Catala for statutes) into compact core languages that preserve legal features like defaults, exceptions and reversible world-state changes. Presents a working Orlando implementation that models events (e.g., “Alice dies”) and prunes interest trees, and Catala’s default calculus that resolves scoped overrides. Claims include machine-checkable proofs of legal theorems (e.g., single ownership) and a roadmap to an LLVM‑style shared IR and tools.
AI-written summary · about