A general approach to define binders using matching logic

Chen, Xiaohong; Roşu, Grigore

Permalink

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

Description

Title

A general approach to define binders using matching logic

Author(s)

• Chen, Xiaohong
• Roşu, Grigore

Issue Date

2020-03

Keyword(s)

• matching logic
• binders
• lambda calculus
• type system

Abstract

We propose a novel shallow embedding of binders using matching logic, where the binding behavior of object-level binders is obtained for free from the behavior of the built-in existential binder of matching logic. We show that binders in various logical systems such as lambda-calculus, System F, pi-calculus, pure type systems, etc., can be defined in matching logic. We show the correctness of our definitions by proving conservative extension theorems, which state that a sequent/judgment is provable in the original system if and only if it is provable in matching logic. An appealing aspect of our embedding of binders in matching logic is that it yields models to all binders, also for free. We show that models yielded by matching logic are deductively complete to the formal reasoning in the original systems. For lambda-calculus, we further show that the yielded models are representationally complete---a desired property that is not enjoyed by many existing lambda-calculus semantics.

Type of Resource

text

Language

en

Permalink

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

Owning Collections