Loading...
Please wait, while we are loading the content...
Similar Documents
A system of interaction and structure IV: The exponentials and decomposition (2007)
| Content Provider | CiteSeerX |
|---|---|
| Author | Straßburger, Lutz Guglielmi, Alessio |
| Description | We study a system, called NEL, which is the mixed commutative/non-commutative linear logic BV augmented with linear logic’s exponentials. Equivalently, NEL is MELL augmented with the non-commutative self-dual connective seq. In this paper, we show a basic compositionality property of NEL, which we call decomposition. This result leads to a cut-elimination theorem, which is proved in the next paper of this series. To control the induction measure for the theorem, we rely on a novel technique that extracts from NEL proofs the structure of exponentials, into what we call!-?-Flow-Graphs. |
| File Format | |
| Language | English |
| Publisher Date | 2007-01-01 |
| Publisher Institution | IN THE SECOND ROUND OF REVISION FOR MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE |
| Access Restriction | Open |
| Subject Keyword | Cut-elimination Theorem Novel Technique Induction Measure Structure Iv Non-commutative Self-dual Connective Seq Basic Compositionality Property Linear Logic Exponential Next Paper |
| Content Type | Text |
| Resource Type | Article |
