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 machine-checkable 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.

Name thesis:degree_name

Ph.D.

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2023

Author dc:creator

• Chen, Xiaohong

Contributors dc:contributor

• Roşu, Grigore
• Meseguer, José
• Parthasarathy, Madhusudan
• Veanes, Margus

• Logic
• Completeness
• Theorem Proving
• Proof Generation
• Proof Checking

Statement dc:rights

• Copyright 2023 Xiaohong Chen

Language dc:language

en, eng

Handle dc:identifier

https://hdl.handle.net/2142/121403

OAI record oai:identifier

https://www.ideals.illinois.edu/oai-pmh?verb=GetRecord&metadataPrefix=etdms&identifier=oai%3Awww.ideals.illinois.edu%3A2142%2F121403