@article{DBLP:journals/mscs/KanovichKNS19, author = {Kanovich, Max and Kuznetsov, Stepan and Nigam, Vivek and Scedrov, Andre}, title = {Subexponentials in non-commutative linear logic}, journal = {Mathematical Structures in Computer Science}, volume = {29}, number = {8}, pages = {1217--1249}, year = {2019}, doi = {10.1017/S0960129518000117}, url = {https://doi.org/10.1017/S0960129518000117}, } @inproceedings{kanovich18ijcar, author = {Kanovich, Max and Kuznetsov, Stepan and Nigam, Vivek and Scedrov, Andre}, title = {A Logical Framework with Commutative and Non-commutative Subexponentials}, booktitle = {Automated Reasoning - 9th International Joint Conference, {IJCAR} 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings}, pages = {228--245}, year = {2018}, abstract = {Logical frameworks allow the specification of deductive systems usingthe same logical machinery. Linear logical frameworks have been successfullyused for the specification of a number of computational, logics and proofsystems. Its success relies on the fact that formulas can be distinguished as linear,which behave intuitively as resources, and unbounded, which behave intuitionistically.Commutative subexponentials enhance the expressiveness of linear logicframeworks by allowing the distinction of multiple contexts. These contexts maybehave as multisets of formulas or sets of formulas. Motivated by applicationsin distributed systems and in type-logical grammar, we propose a linear logicalframework containing both commutative and non-commutative subexponentials.Non-commutative subexponentials can be used to specify contexts which behaveas lists, not multisets, of formulas. In addition, motivated by our applications intype-logical grammar, where the weakenening rule is disallowed, we investigatethe proof theory of formulas that can only contract, but not weaken. In fact, ourcontraction is non-local. We demonstrate that under some conditions such formulasmay be treated as unbounded formulas, which behave intuitionistically.}, doi = {10.1007/978-3-319-94205-6\_16}, url = {https://doi.org/10.1007/978-3-319-94205-6\_16}, } @article{kanovich18mscs, author = {Kanovich, Max and Kuznetsov, Stepan and Nigam, Vivek and Scedrov, Andre}, title = {Subexponentials in non-commutative linear logic}, journal = {Mathematical Structures in Computer Science}, year = {2018}, abstract = {Linear logical frameworks with subexponentials have been used for the specification of,among other systems, proof systems, concurrent programming languages and linearauthorisation logics. In these frameworks, subexponentials can be configured to allow or notfor the application of the contraction and weakening rules while the exchange rule canalways be applied. This means that formulae in such frameworks can only be organised assets and multisets of formulae not being possible to organise formulae as lists of formulae.This paper investigates the proof theory of linear logic proof systems in thenon-commutative variant. These systems can disallow the application of exchange rule onsome subexponentials. We investigate conditions for when cut elimination is admissible inthe presence of non-commutative subexponentials, investigating the interaction of theexchange rule with the local and non-local contraction rules. We also obtain some newundecidability and decidability results on non-commutative linear logic with subexponentials.}, doi = {10.1017/S0960129518000117}, url = {https://doi.org/10.1017/S0960129518000117}, }