University of Illinois Urbana-Champaign

Matching μ-Logic

Chen, Xiaohong

Content Files
CHEN-DISSERTATION-2023.pdf

Permalink

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

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
Handle URL
https://hdl.handle.net/2142/121403
Copyright and License Information
Copyright 2023 Xiaohong Chen

Owning Collections

Graduate Dissertations and Theses at Illinois PRIMARY
Graduate Theses and Dissertations at Illinois