# Questions tagged [linear-logic]

Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter. Ideas from linear logic have been influential in fields such as programming languages, game semantics, and quantum physics, as well as linguistics, particularly because of its emphasis on resource-boundedness, duality, and interaction.

38 questions
Filter by
Sorted by
Tagged with
39 views

### Linearly distributive categories: Principles of excluded middle and contradiction

1. Context Let $(\mathscr{C}, \otimes, \top, \oplus, \bot, \delta ^l, \delta^r)$ be a linearly distributive category. Let $(S,S', \alpha, \beta, \alpha‘, \beta‘)$ be a negation on $\mathscr{C}$. This ...
164 views

### Linear logic and linearly distributive categories

1. Context On page two of the introduction to their paper Weakly distributive categories on linearly distributive categories Cockett and Seely write: It turns out that these weak distributivity maps, ...
85 views

### Why is multiplicative disjunction called "par" in linear logic?

In linear logic multiplicative disjunction is often called par. This terminology goes back at least to Girard's seminal text Linear logic. I vaguely remember that I read that "par" is an ...
52 views

### Is $A ⅋ (B \otimes C) \vdash (A⅋B) \otimes C$ provable in MLL?

Consider the multiplicative fragment of linear logic (MLL) which only consists of the multiplicative connectives tensor and par together with the inference rules axiom, cut, $\otimes$ and ⅋. I was ...
161 views

123 views

62 views

### Logics for resource control over time

I'm studying proof theory and I've seen that linear logic can be used as a "way" to control resources usage, since by the propositions-as-types it is equivalent to the linear lambda calculus. Is ...
228 views

### Intuitionistic Linear Logic

I am currently going through some papers that use the "intuitionistic version" of Girard's Linear Logic. The problem is that I seem to find very little literature on it. There is a lot done on Linear ...
### In linear logic sequent calculus, can $\Gamma \vdash \Delta$ and $\Sigma \vdash \Pi$ be combined to get $\Gamma, \Sigma \vdash \Delta, \Pi$?
Linear logic is a certain variant of sequent calculus that does not generally allow contraction and weakening. Sequent calculus does admit the cut rule: given contexts $\Gamma$, $\Sigma$, $\Delta$, ...
I'm $\DeclareMathOperator{\par}{\unicode{8523}}$ trying to wrap my mind around the $\par$ ("par") operator of linear logic. The other connectives have simple resource interpretations ($A\otimes B$ ...