Difference between revisions of "Applicative Matching Logic"

From FSL
Jump to: navigation, search
(Created page with "<private> == POPL 2020 Submission == <pubbib id='chen-rosu-2020-popl-submission' template='PubDefaultWithAbstractAndTitle'/> </private>")
 
 
Line 1: Line 1:
 +
== Technical Report ==
 +
<pubbib id='chen-rosu-2019-trb' template='PubDefaultWithAbstractAndTitle'/>
 
<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>

Latest revision as of 14:41, 27 July 2019

[edit] Technical Report

Applicative Matching Logic
Xiaohong Chen and Grigore Rosu
Technical Report http://hdl.handle.net/2142/104616, July 2019
Abstract. This paper proposes a novel 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


Personal tools
Namespaces

Variants
Actions
Navigation