Applicative matching logic

Chen, Xiaohong; Roşu, Grigore

Permalink

https://hdl.handle.net/2142/104616 Copy

Description

Title

Applicative matching logic

Author(s)

• Chen, Xiaohong
• Roşu, Grigore

Issue Date

2019-07-31

Keyword(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.

Type of Resource

text

Language

en

Permalink

http://hdl.handle.net/2142/104616

Owning Collections