Files in this item

FilesDescriptionFormat

application/pdf

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

Description

Title:Applicative matching logic
Author(s):Chen, Xiaohong; Rosu, 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
Type:Text
Language:English
URI:http://hdl.handle.net/2142/104616
Date Available in IDEALS:2019-07-31


This item appears in the following Collection(s)

Item Statistics