# Difference between revisions of "Applicative Matching Logic"

From FSL

Line 2: | Line 2: | ||

<pubbib id='chen-rosu-2019-trb' template='PubDefaultWithAbstractAndTitle'/> | <pubbib id='chen-rosu-2019-trb' template='PubDefaultWithAbstractAndTitle'/> | ||

+ | <private> | ||

+ | == LICS 2020 Submission == | ||

+ | <pubbib id='chen-rosu-2020-lics-submission' template='PubDefaultWithAbstractAndTitle'/> | ||

+ | </private> | ||

<private> | <private> | ||

== ESOP 2020 Submission == | == ESOP 2020 Submission == |

## Latest revision as of 01:43, 16 January 2020

## [edit] Technical Report

**Applicative Matching Logic: Semantics of K**- Xiaohong Chen and Grigore Rosu
http://hdl.handle.net/2142/104616, July 2019**Technical Report**

*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.

- PDF, Matching Logic, DOI, BIB