# Tagged Questions

Logic with limited contraction and weakening.

172 views

### Can you explain an intuition behind Coherent Spaces?

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 ...
131 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 ...
128 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 ...
260 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. ...
2k 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 ...
333 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\...
579 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 ...