# 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
2 votes
0 answers
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 ...
• 1,938
6 votes
1 answer
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, ...
• 1,938
5 votes
1 answer
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 ...
• 1,938
3 votes
1 answer
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 ...
• 315
6 votes
0 answers
161 views

• 77
4 votes
1 answer
123 views

• 4,798
5 votes
0 answers
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 ...
4 votes
1 answer
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 ...
• 1,125
6 votes
1 answer
259 views

### 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$, ...
• 8,915
28 votes
6 answers
5k views

### What is the intuition behind the "par" operator in linear logic?

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$ ...
• 383