Difference between revisions of "Applicative Matching Logic"
From FSL
| Line 1: | Line 1: | ||
== Technical Report == | == Technical Report == | ||
<pubbib id='chen-rosu-2019-trb' template='PubDefaultWithAbstractAndTitle'/> | <pubbib id='chen-rosu-2019-trb' template='PubDefaultWithAbstractAndTitle'/> | ||
| + | |||
| + | <private> | ||
| + | == ESOP 2020 Submission == | ||
| + | <pubbib id='chen-rosu-2020-esop-submission' template='PubDefaultWithAbstractAndTitle'/> | ||
| + | </private> | ||
<private> | <private> | ||
== POPL 2020 Submission == | == POPL 2020 Submission == | ||
<pubbib id='chen-rosu-2020-popl-submission' template='PubDefaultWithAbstractAndTitle'/> | <pubbib id='chen-rosu-2020-popl-submission' template='PubDefaultWithAbstractAndTitle'/> | ||
</private> | </private> | ||
Revision as of 16:14, 25 November 2019
Technical Report
- Applicative Matching Logic: Semantics of K
- Xiaohong Chen and Grigore Rosu
- Technical Report http://hdl.handle.net/2142/104616, July 2019
- 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
