Last call to make your voice heard! Our 2022 Developer Survey closes in less than a week. Take survey.

# Tag Info

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

The intuition behind coherence spaces is that the elements of a coherence space represent observations of some underlying data, and the coherence relation tells you whether two observations could have ...
• 31.6k
Accepted

### What is the intuition behind linear logic?

I'm not sure this question is ideal for CSTheory, but given that it's already gathering upvotes, here is an answer somebody might have given had the question been posted on cs.stackexchange. In ...
• 10.3k

### How does linear logic achieve resource management?

The following answers your first two questions. It seems to me that you're working under the assumption that propositional linear logic is a 4-valued logic, in the same sense that propositional ...
• 4,823
Accepted

### Recursive types and the empty type

First, note that nothing turns on the presence or absence of the empty type: if you have a nonlinear calculus with function types and unrestricted recursive types, then it is inconsistent. Indeed, ...
• 31.6k
Accepted

### Can you assign a type to any term of the λEA-calculus?

For question 1, the answer is no, and is no for almost any type discipline (except certain intersection types): the fact that a term is (strongly or weakly) normalizable does not imply in general that ...
• 4,823
Accepted

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

I don't want to make a statement about "all linear lambda calculi" since it's hard to make that precise, but for pure linear lambda-calculus the answer is yes. One way to enforce linearity in pure ...
• 4,289

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

I always had trouble forming an intuition for coherence spaces, until I became more familiar with domain theory and read Girard's "The System F of variable types, fifteen years later". Coherence ...
Accepted

### Parametricity of Linear Logic

Various people are interested in proving this sort of thing. Neel Krishnaswami mentioned this particular theorem here. I’ve also seen Frank Pfenning give some cool examples for ordered logics. For ...
• 185
Accepted

### A stronger multiplexing rule for soft linear logic?

Your rule $(\ast)$ is sometimes referred to as "absorption". I think the first who considered it was Jean-Marc Andreoli in his paper on focusing proofs. Indeed, it makes a lot of sense in proof ...
• 4,823

### Algebraic account of Gaussian elimination?

You really should read Gowers' essay carefully - it cleanly details the reasons why you need a basis in general. So if there is going to be an algebraic account of Gauss-Jordan, it will necessarily ...
• 1,490

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

No one knows if there are connections between GoI and GCT. It's quite plausible, since both are used to analyze complexity, and since GoI is formulated in terms of monoidal categories and GCT is ...
• 31.6k
Accepted

### Type theory for memory safe data structures

There has been a lot of work around the idea of statically checking the memory safety properties of programs. Francois Pottier give an excellent overview of various approaches in this presentation. ...
• 13.1k

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

I extend what I wrote as a comment. As there is a great number of cases in the proof, I only give an idea of why this transformation terminates. The short answer is: In the case promotion vs ...
• 1,855
Accepted

### Does this variant of Multiplicative Linear Logic with mix rule enjoy cut elimination?

For question 1, if by "deadlock" you mean "non-trivial vicious circle", then the answer is obviously yes, simply because a non-trivial vicious circle cannot be typed: you will have a cut between a ...
• 4,823
Accepted

### Is the set of Multiplicative Proof Nets a proper subset of set of well formed single-agent Interaction Nets?

Your observation about cut-elimination being faithfully represented in the unlabelled interaction nets is correct. However, the answer to your question is no. Let us call $\delta$ the unique agent ...
• 4,823
Here is a partial answer: the rule $(*)$ is not conservative over SLL. Indeed, McKinley showed that soft linear set theory with unrestricted comprehension is nontrivial — but adding $(*)$ makes ...