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

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 ...
user avatar
11 votes
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 ...
user avatar
10 votes

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 ...
user avatar
9 votes
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, ...
user avatar
9 votes
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 ...
user avatar
8 votes
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 ...
user avatar
7 votes

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 ...
user avatar
7 votes
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 ...
user avatar
7 votes
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 ...
user avatar
5 votes

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 ...
user avatar
5 votes

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 ...
user avatar
5 votes
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. ...
user avatar
  • 13.1k
4 votes

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 ...
user avatar
  • 1,855
4 votes
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 ...
user avatar
3 votes
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 ...
user avatar
2 votes

A stronger multiplexing rule for soft linear logic?

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 ...
user avatar
2 votes

How could one define a language based on the Calculus of Constructions, but with fixed points and EAL-style duplication restrictions?

Dependency is interesting because of equality, and equality is adjoint to contraction. As a result, substructural calculi (which in general omit contraction) do not have an obvious notion of equality. ...
user avatar

Only top scored, non community-wiki answers of a minimum length are eligible