# Questions tagged [linear-logic]

Logic with limited contraction and weakening.

34 questions
Filter by
Sorted by
Tagged with
218 views

### An untyped lambda calculus for explicit memory management

I am trying to find resources on a lambda calculus one would use for explicit memory management, assuming there is such a calculus. The concept is as follows: one takes untyped lambda calculus, ...
• 291
1 vote
179 views

### Which are the rules for minimal logic in both sequent calculus and natural deduction styles?

Are there any references I could use which explictly contain the rules for minimal logic, both as a sequent calculus and in natural deduction? (Doesn't need to be the same reference for both!) To give ...
• 387
235 views

### True origin story of linear logic?

When I was a master's student in Paris I was exposed to the following standard narrative: "J.-Y. Girard invented coherence spaces, then he noticed the decomposition $A \to B~=~!A \multimap B$ and ...
268 views

### Is there any logical concept that Rust lifetimes correspond to?

We're all used to invoking Curry–Howard to find correspondences between type systems and logical systems. Rust has a very interesting type system, that is typically compared to a substructural logic. ...
• 487
86 views

### Is logic in computation of computation constructivist?

Is logic in computation of computation constructivist? I think so, because dynamic languages ​​are comparable to constructivist set theory (try a demonstration of the axiom of choice in computing: it ...
70 views

### What does impredicativity mean in substructural and co-intuitionistic logics?

Predicative foundations puts restrictions on power sets and function sets. Entirely apart from the philosophy predicative theories are a lot easier to prove things about and this sounds interesting to ...
364 views

### How does linear logic achieve resource management?

TL;DR: I want to know how linear logic works. Sorry for the long question, I try to explain myself as best as I can in hopes of receiving good answers, especially because I don't know anyone else to ...
218 views

### Do Banach spaces and linear contraction maps form a model of ILL with an exponential?

Recently, I read on the nLab that the category of Banach spaces and linear contractions is small complete, small cocomplete, and monoidal closed. This means that Banach spaces and short linear maps ...
• 32.8k
217 views

• 32.8k
409 views

### Why does this cut elimination procedure terminate (contraction case)?

In Melliès’ survey Categorical Semantics of Linear Logic, a cut elimination procedure for intuitionistic linear logic is given which includes the following case: 3.9.3 Promotion vs. contraction The ...
1k views

### How to think about coherent spaces intuitively?

Linear Logic is interpreted using coherent spaces, and they feature prominently in Girard's papers. I know all the three main ways to formally define them, and they don't really pose any problem to ...
• 487
669 views

### Can all linear lambda calculi be linearity checked syntactically?

Given a lambda calculus with explicit linearity and usual application and abstraction, can the linearity check be done on an untyped syntax tree if we keep track of the structural types? Are the ...
252 views

### Are there links between Geometry of Interaction and Geometric Complexity Theory?

I'm very much a novice in these subjects, but Geometry of Interaction and Geometric Complexity Theory seem to speak similar language and have vaguely similar goals. Am I not mistaken? Are there any ...
• 487
380 views

### Type theory for memory safe data structures

Data structures such as a doubly linked list and a B+ tree have blocks of memory that have multiple pointers to it. This creates the risk that a bug will allow memory to be accessed after being freed. ...
3k views

### How should I think about proof nets?

In his answer to this question, Stephane Gimenez pointed me to a polynomial-time normalization algorithm for proofs in linear logic. The proof in Girard's paper uses proof nets, which are an aspect of ...
• 32.8k
532 views

### Is MALL + unrestricted recursive types Turing-complete?

If you look at the recursive combinators in the untyped lambda-calculus, such as the Y combinator or the omega combinator:  \begin{array}{lcl} \omega & = & (\lambda x.\,x\;x)\;(\lambda x.\,x\...
• 32.8k
863 views

### Automated theorem proving in linear logic

Is automatic theorem proving and proof searching easier in linear and other propositional substructural logics which lack contraction? Where can I read more about automatic theorem proving in these ...
• 4,041
476 views

• 32.8k