Turning Catala into a Proof Platform for the Law
summary
Catala becomes a proof platform that uses proof-by-refinement to simplify programs while preserving semantics, generating no-empty/no-conflict VCs for default terms and sending them to a Z3 encoding; VC generation and a basic Z3 backend are implemented, Z3 models produce concrete counterexample error reports, and a conference demo detects and helps fix an eligibility ambiguity. Full mechanized correctness proofs and a complete Catala→SMT encoding are work in progress, plus support for other provers.
AI-written summary · about
chapters (10)
- 0:00Catala as proof platform
- 1:06Legal expert systems challenges
- 3:13Formal verification goals
- 4:37Catala design and legal code
- 7:25Proof by refinement strategy
- 8:08Default terms in Catala
- 10:59Verification conditions for defaults
- 13:46Implementation and future work
- 15:30Live demo of Catala
- 18:39Q&A
related talks
20mModern DSL compiler architecture in OCaml our experience with Catala
19mAutomated Verification of Fundamental Algebraic Laws
18mAutomated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic(…)
36mMcTT: Building A Correct-By-Construction Proof Checker For Martin-Loef Type Theory
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
46mMechanizing Abstract Interpretation
59mCoq to C Translation with Partial Evaluation + Counterexample Generation
15mTabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits