Designs for the L4 Contract Programming Language Based on Deontic Modal Logic
summary
Proposes L4, a DSL that encodes obligations, permissions and prohibitions via the deontic modal μ-calculus and compiles to automata for decidable trace satisfaction and static checks that flag inconsistency, incompleteness, goal satisfaction, and policy compliance. Implementation work targets Haskell, the project is open source under legalese, and the design includes a concrete blame assignment semantics plus backends that can emit English or Ethereum bytecode so contracts can be audited and executed.
AI-written summary · about
chapters (12)
- 0:00Introduction to Legalese
- 0:55The goal of legal DSLs
- 1:28Formal verification in law
- 2:51Smart contract legal modeling
- 3:13DSL vs Solidity
- 5:26Logic-based formalism
- 9:20Trace semantics and verification
- 9:47Automata rendering
- 12:38Attributing responsibility
- 13:53Composition of contracts
- 15:51Practical NDA example
- 17:08Implementation and future
related talks
45mLogic Meta Programming for Functional Languages
18mEpistemic Logic for Polyglots (Short Paper)
23mUsing LLM Generated Formal Specs to Prevent the Next DeFi Hack
29mSynthesizing Axiomatizations using Logic Learning
20mA Dependent Type Theory for Meta-programming with Intensional Analysis
35mDesigning Domain-Specific Languages: A Comparison of Three Approaches by Example
18mA modal deconstruction of Löb induction
50mA Type-Theoretic Framework for Certified Meta-programming