Kleene Algebra Modulo Theories: A Framework for Concrete KATs
summary
Framework that turns a KAT into a concrete, decidable KAT when you supply three things: primitive actions/tests with weakest preconditions, sound/complete axioms and an ordering on those preconditions, and a satisfiability oracle. Implementation in OCaml normalizes terms, encodes test satisfiability to Z3 and recovers existing KATs (NetKAT, bitvectors, monotonic naturals, sets, maps); completeness and decidability hold under the stated conditions. Current limits: it records tracing every action (too fine-grained) and uses rewriting (slower than automata); code and examples are on GitHub and run.
AI-written summary · about
chapters (8)
- 0:00Kleene Algebra with Tests intro
- 3:54Abstract KAT limitations
- 6:01NetKAT in networking
- 8:47Building specialized KATs
- 9:27KMT framework for KATs
- 12:54KMT limitations and future
- 14:00Applications beyond networking
- 15:03Q&A
related talks
20mAlgebras for Deterministic Computation are Inherently Incomplete
20mA Taxonomy of Hoare-Like Logics
12mContextual Algebraic Theories: Generic Boilerplate beyond Abstraction
32mA mechanised and constructive reverse analysis of soundness and completeness of b...
23mImplementing a category-theoretic framework for typed abstract syntax
22mTurning Catala into a Proof Platform for the Law
20mA Dependent Type Theory for Meta-programming with Intensional Analysis
29mSynthesizing Axiomatizations using Logic Learning