PhD Thesis: Matching µ-Logic

Matching µ-logic is proposed as a unifying logic for specifying and reasoning about programs and programming languages. The logic uses its formulas, called patterns, to uniformly express programs' static structures, dynamic behaviors, and logical constraints. Unlike traditional approaches where different aspects of programming languages require separate formalisms, matching µ-logic provides a single framework in which program configurations, execution rules, and correctness properties can all be expressed as patterns. The dissertation was completed at the University of Illinois Urbana-Champaign under the direction of Professor Grigore Rosu, and represents a culmination of years of research into the foundations of the K semantic framework. The core insight is that pattern matching, when combined with fixpoint operators, yields a logic of remarkable expressive power that subsumes many existing logics used in programming language theory and formal verification.

The dissertation begins by establishing the mathematical foundations necessary for understanding matching µ-logic. It covers basic mathematics, first-order logic, and first-order logic extended with least fixpoints, providing the reader with a self-contained treatment of the prerequisite material. Second-order logic is also discussed to contextualize the expressive power of matching µ-logic relative to classical logical systems. The treatment of equational specifications and initial algebra semantics demonstrates how algebraic approaches to programming language semantics can be captured within the matching logic framework. These foundational chapters serve not only as background material but also as a demonstration of how each of these classical logical systems can be viewed as a special case or fragment of matching µ-logic.

Matching µ-logic captures modal µ-logic, temporal logics, and reachability logic as instances, providing a single proof system for reasoning about all of them.

The core syntax of matching µ-logic is built from element variables, set variables, constant symbols, and several constructors: application (written as juxtaposition), bottom ($\bot$), implication ($\to$), existential quantification ($\exists$), and the least fixpoint µ-binder ($\mu X . \varphi$). From these primitives, the standard logical connectives such as negation ($\neg \varphi \equiv \varphi \to \bot$), disjunction ($\varphi_1 \lor \varphi_2$), conjunction ($\varphi_1 \land \varphi_2$), and the definedness symbol ($\lceil \varphi \rceil$) are derived. The definedness pattern $\lceil \varphi \rceil$ is a predicate pattern that holds when $\varphi$ is matched by at least one element. The greatest fixpoint operator $\nu X . \varphi$ is defined dually as $\neg \mu X . \neg \varphi[\neg X / X]$. This minimal set of primitives keeps the proof system small while enabling the encoding of complex logical and computational concepts.

The Hilbert-style proof system of matching µ-logic consists of a small collection of proof rules that are remarkably simple yet sufficient for reasoning about programs and languages. The proof system defines a provability relation where a set of patterns, called a theory, serves as the collection of axioms from which theorems are derived. The proof rules include standard propositional reasoning (including modus ponens: from $\varphi$ and $\varphi \to \psi$, derive $\psi$), quantifier rules for both element and set variables (including universal generalization: from $\varphi$, derive $\forall x.\, \varphi$), the Knaster-Tarski rule for fixpoint reasoning (from $\varphi[\psi/X] \to \psi$, derive $\mu X.\, \varphi \to \psi$), and rules for framing (from $\varphi_1 \to \varphi_2$, derive $C[\varphi_1] \to C[\varphi_2]$ for any context $C$) that support local reasoning similar to separation logic. A key property established in the dissertation is local completeness: the proof system is complete for proving the validity of patterns in any given matching µ-logic theory. This means that any semantically valid statement about programs can, in principle, be formally proved using the proof rules.

The dissertation demonstrates the remarkable expressive power of matching µ-logic by showing how numerous important logics arise as instances or fragments. Modal mu-calculus, the foundational logic for model checking, is captured by interpreting modal operators as patterns involving application. Temporal logics including LTL and CTL*, which are widely used for specifying and verifying reactive systems, can be encoded using the fixpoint operators. Reachability logic, where claims of the form $\varphi \Rightarrow^\bullet \psi$ assert that any configuration matching $\varphi$ eventually reaches one matching $\psi$, is shown to be a natural fragment of matching µ-logic that subsumes Hoare logic (where $\{P\}\; C \;\{Q\}$ is expressed as $\langle P, C \rangle \Rightarrow^\bullet \langle Q, \cdot \rangle$). Separation logic with recursive predicates, where the separating conjunction $\varphi_1 \ast \varphi_2$ asserts disjoint heap decomposition, is also captured. These embeddings are not mere theoretical exercises; they demonstrate that a single proof infrastructure can serve all these verification paradigms.

A major contribution of the dissertation is Applicative Matching mu-Logic (AML), a simplified instance of matching µ-logic that retains all of its expressive power. In AML, sorts and many-sorted symbols are eliminated because they are definable using axioms and theories, resulting in a much simpler syntax and semantics. Despite this simplification, AML can encode the full matching µ-logic through a faithful translation. The dissertation presents an encoding of matching µ-logic into AML and implements a proof checker in approximately 200 lines of code using the Metamath proof verification system. This extremely compact proof checker demonstrates the practical viability of the approach: the trust base for verifying program correctness is minimal, consisting only of a small, auditable proof checker and the formal semantics of the programming language in question.

The dissertation studies automated reasoning for matching µ-logic, with a particular focus on fixpoint reasoning. A set of high-level automated proof rules is proposed that can be applied to many matching µ-logic theories, thus enabling automated reasoning in them. The fixpoint reasoning framework is especially important because fixpoints arise naturally in programming language semantics: recursive data types (e.g., $\mathsf{List} = \mu X.\, (\mathsf{nil} \vee \mathsf{cons}(\mathsf{Nat}, X))$), loops, recursive functions, and infinite behaviors of reactive systems all involve fixpoints. The proposed proof rules include techniques for circular reasoning, where a proof obligation involving a fixpoint can be discharged by assuming the conclusion and showing that it is a pre-fixpoint or post-fixpoint of the relevant operator. These automated proof rules bridge the gap between the theoretical completeness of the proof system and practical tool support.

The dissertation addresses proof-certifying program execution, where the correctness of an execution or verification task is established by an AML proof object serving as a machine-checkable correctness certificate. When a program is executed according to its formal semantics (defined as a matching µ-logic theory), each step of the execution corresponds to a proof step in matching µ-logic. The entire execution trace can thus be assembled into a complete proof object that certifies the result of the computation. This approach is language-independent: it works for any programming language whose formal semantics has been defined in the K framework, including languages like C, Java, JavaScript, Python, Solidity, and the EVM. The proof objects can be independently checked by the compact AML proof checker, providing strong correctness guarantees without trusting the execution engine itself.

The 200-line AML proof checker implemented in Metamath represents a minimal trust base: if the formal semantics and the proof checker are correct, then any verified execution is guaranteed to be correct.

The dissertation's results have profound implications for the K semantic framework and its applications. Since K uses matching µ-logic as its logical foundation, the proof generation and verification infrastructure developed in the dissertation applies directly to all languages defined in K. This means that formal verification tools generated by K, including program verifiers, symbolic executors, and model checkers, can produce machine-checkable proof certificates for their results. The work laid the groundwork for the Proof of Proof concept developed by Pi2 Labs, where succinct cryptographic proofs (such as zero-knowledge proofs) are generated for the verification of matching logic proof objects, enabling trustless verifiable computing across any programming language. The dissertation thus represents both a fundamental theoretical contribution to logic and a practical foundation for next-generation verified and verifiable computing infrastructure.

In conclusion, the dissertation establishes matching µ-logic as a viable and powerful unifying foundation for programming languages and formal methods. By demonstrating that a single logic with a compact proof system can capture the semantics of arbitrary programming languages and subsume the major verification logics, it simplifies the landscape of formal methods and opens the door to universal tools that work across all languages. The practical implementation via AML and the 200-line proof checker validates the approach, showing that theoretical elegance translates into practical minimality. The work connects deeply to both the theory of programming languages and to emerging applications in blockchain, verifiable computing, and zero-knowledge proofs, positioning matching µ-logic as a cornerstone technology for trustworthy computation.