University of Illinois Urbana-Champaign

Applicative matching logic

Chen, Xiaohong; Roşu, Grigore

Content Files
chen-rosu-2019-trb.pdf

Permalink

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

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
Date of Ingest
2019-07-31T12:23:18Z
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
Genre of Resource
Technical Report
Language
en
Permalink
http://hdl.handle.net/2142/104616

Owning Collections

Research and Tech Reports - Computer Science PRIMARY