@techreport{chen-rosu-2019-trb,
author = {Xiaohong Chen and Grigore Ro\c{s}u},
title = {Applicative Matching Logic: Semantics of K},
author_id = {Xiaohong Chen and Grigore Rosu},
category = {fsl,matching_logic,program_verification},
project_url = {http://www.matching-logic.org},
project_name = {Matching Logic},
institution = {University of Illinois at Urbana-Champaign},
month = {July},
year = {2019},
number = {http://hdl.handle.net/2142/104616},
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.
},
hidden = {false},
}