2026-09-21T07:36:01Z https://www.ideals.illinois.edu/oai-pmh

oai:www.ideals.illinois.edu:2142/121403 2023-12-13 col_2142_5131 col_2142_10761 com_2142_5130 com_2142_10755 com_2142_234

Roşu, Grigore Roşu, Grigore Meseguer, José Parthasarathy, Madhusudan Veanes, Margus 2023-08 application/pdf en text Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2023-12-04 without embargo terms The student, Xiaohong Chen, accepted the attached license on 2023-05-24 at 18:13. The student, Xiaohong Chen, submitted this Dissertation for approval on 2023-05-24 at 18:24. This Dissertation was approved for publication on 2023-05-26 at 09:11. DSpace SAF Submission Ingestion Package generated from Vireo submission #19392 on 2023-12-04 at 16:59:48 Matching μ-Logic Chen, Xiaohong 2023-05-26 Logic Completeness Theorem Proving Proof Generation Proof Checking 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. Text eng https://hdl.handle.net/2142/121403 Copyright 2023 Xiaohong Chen Ph.D. Dissertation Computer Science University of Illinois at Urbana-Champaign Computer Science