Files in this item



application/pdfchen-rosu-2019-trb.pdf (966kB)
(no description provided)PDF


Title:Applicative matching logic
Author(s):Chen, Xiaohong; Roşu, Grigore
Subject(s):language frameworks
formal semantics
type systems
K framework
Abstract:This paper proposes a logic for programming languages, which is both simple and expressive, to serve as a foundation for language semantics frameworks. Matching mu-logic has been recently proposed as a unifying foundation for programming languages, specification and verification. It has been shown to capture several logics important for programming languages, including first-order logic with least fixpoints, separation logic, temporal logics, modal mu-logic, and importantly, reachability logic, a language-independent logic for program verification that subsumes Hoare logic. This paper identifies a fragment of matching mu-logic called applicative matching logic (AML), which is much simpler and thus more appealing from a foundational perspective, yet as expressive as matching mu-logic. Several additional logical frameworks fundamental for programming languages are shown to be faithfully captured by AML, including many- and order-sorted algebras, lambda-calculus, (dependent) type systems, evaluation contexts, and rewriting. Finally, it is shown how all these make AML an appropriate underlying logic foundation for complex language semantics frameworks, such as K.
Issue Date:2019-07-31
Genre:Technical Report
Date Available in IDEALS:2019-07-31

This item appears in the following Collection(s)

Item Statistics