Difference between revisions of "A General Approach to Define Binders Using Matching Logic"

From FSL
Jump to: navigation, search
 
Line 1: Line 1:
 
== ICFP 2020 ==
 
== ICFP 2020 ==
<pubbib id='chen-rosu-2020-icfp-submission' template='PubDefaultWithAbstractAndTitle'/>
+
<pubbib id='chen-rosu-2020-icfp' template='PubDefaultWithAbstractAndTitle'/>
 
== Technical Report ==
 
== Technical Report ==
 
<pubbib id='chen-rosu-2020-tr' template='PubDefaultWithAbstractAndTitle'/>
 
<pubbib id='chen-rosu-2020-tr' template='PubDefaultWithAbstractAndTitle'/>

Latest revision as of 20:57, 21 June 2020

[edit] ICFP 2020

A General Approach to Define Binders Using Matching Logic
Xiaohong Chen and Grigore Rosu
ICFP'20, ACM/IEEE 4, pp 1-32. 2020
Abstract. We propose a novel definition of binders using matching logic, where the binding behavior of object-level binders is directly inherited from the built-in exists binder of matching logic. We show that the behavior of binders in various logical systems such as lambda-calculus, System F, pi-calculus, pure type systems, can be axiomatically defined in matching logic as notations and logical theories. 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, in the corresponding theory. Our matching logic definition of binders also yields models to all binders, which are deductively complete with respect to 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. This work is part of a larger effort to develop a logical foundation for the programming language semantics framework K (http://kframework.org).
PDF, Slides(PPTX), Slides(PDF), Matching Logic, ICFP'20, BIB

[edit] Technical Report

A General Approach to Define Binders Using Matching Logic
Xiaohong Chen and Grigore Rosu
Technical Report http://hdl.handle.net/2142/106608, June 2020
Abstract. We propose a novel definition of binders using matching logic, where the binding behavior of object-level binders is directly inherited from the built-in exists binder of matching logic. We show that the behavior of binders in various logical systems such as lambda-calculus, System F, pi-calculus, pure type systems, can be axiomatically defined in matching logic as notations and logical theories. 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, in the corresponding theory. Our matching logic definition of binders also yields models to all binders, which are deductively complete with respect to 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. This work is part of a larger effort to develop a logical foundation for the programming language semantics framework K (http://kframework.org).
PDF, Matching Logic, DOI, BIB

Personal tools
Namespaces

Variants
Actions
Navigation