Matching µ-Logic

We present matching µ-logic, which is a unifying logic for specifying and reasoning about programs and programming languages. Matching µ-logic uses its formulas, called patterns, to uniformly express programs’ static structures, dynamic behaviors, and logical constraints. Programming languages can be formally defined as matching µ-logic theories, which include patterns as axioms. The correctness of programming language implementations and tools can be proved using a fixed proof system. These proofs can be encoded as proof objects and automatically checked using a small proof checker.

 

An important feature of matching µ-logic is its µ operator, which provides direct support for specifying fixpoints and thus enables to specify and reason about induction and recursion. We study the proof theory of matching µ-logic and prove a few important completeness results.

 

We study the expressive power of matching µ-logic and show that many important logics, calculi, and foundations of computations, especially those featuring fixpoints/induction/recursion, can be defined as matching µ-logic theories.

 

We study automated reasoning for matching µ-logic, with a focus on fixpoint reasoning. We propose a set of high-level automated proof rules that can be applied to many matching µ-logic theories, and thus enable automated reasoning in them.

 

We propose applicative matching µ-logic, abbreviated as AML, as a simple instance of matching µ-logic that retains all of its expressive power. AML is a fragment of matching µ-logic where we eliminate sorts and many-sorted symbols from matching µ-logic, because they are definable using axioms and theories. We present an encoding of matching µ-logic into AML and implement a 200-line proof checker for AML using Metamath.

 

We study proof-certifying program execution and formal verification, where the correctness of an execution/verification task is established by an AML proof object, serving as a machinecheckable correctness certificate. Our approach is based on the K formal language semantics framework. We design and implement procedures that output AML proof objects for the language-agnostic program interpreter and formal verifier of K, which are parametric in the formal semantics of a programming language. This way, we reduce checking the correctness of a language task (i.e., executing or verifying a program) to checking the corresponding AML proof objects using the proof checker.

 

We hope to demonstrate that matching µ-logic can serve as a unifying foundation for programming, where programming languages are defined as theories, and the correctness of language tools is established by machine-checkable proof objects.