Matching μ-Logic

Chen, Xiaohong

Permalink

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

Description

Title

Matching μ-Logic

Author(s)

Chen, Xiaohong

Issue Date

2023-05-26

Director of Research (if dissertation) or Advisor (if thesis)

Roşu, Grigore

Doctoral Committee Chair(s)

Roşu, Grigore

Committee Member(s)

• Meseguer, José
• Parthasarathy, Madhusudan
• Veanes, Margus

Department of Study

Computer Science

Discipline

Computer Science

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Keyword(s)

• logic
• completeness
• theorem proving
• proof generation
• proof checking

Abstract

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.

Graduation Semester

2023-08

Type of Resource

Thesis

Copyright and License Information

Copyright 2023 Xiaohong Chen

Owning Collections