Matching Logic: Foundation of the K Framework
summary
One formal semantics drives interpreters, verifiers and model checkers: a 5,000‑rule C11 semantics with a >120‑cell configuration compiles to LLVM and yields a native interpreter; the K‑based RV‑Match/KCC tool finds C undefined behavior; an EVM semantics passes the 60,000 official tests and the auto‑generated interpreter is ~25% faster than some ad hoc VMs. Matching Logic uses patterns not predicates, a tiny proof checker prototype (~200 LOC) and least‑fixpoint binders to express verification and model‑checking properties; full completeness is partial.
AI-written summary · about
chapters (16)
- 0:00Start
- 3:20Syntax
- 3:47Version Strategy Annotations
- 4:19Program Configuration
- 5:21Local Rewriting
- 9:19Interpreter
- 10:27Undefined Behavior Detector
- 22:57Derived Constructs
- 24:00Overview
- 24:54The Sealing Operator
- 26:24Functions
- 34:26Transition Systems
- 37:16Completeness
- 43:53Human Readable Semantics
- 45:10Formal Verification of Smart Contracts
- 52:46What Is a Programming Language
related talks
31mProgramming Languages Must Have Formal Semantics. Period.
15mTowards a Unified Proof Framework for Automated Fixpoint Reasoning using Matching Logic
23mVellvm: Formalizing the Informal
23mType-Level Programming with Match Types
01h 06mVerifying a compiler through equational means- 01h 06mVerifying a compiler through equational means
01h 05mAll the Languages Together
30mA Core Language for Extended Pattern Matching and Binding Boolean Expressions