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 ...
Neel Krishnaswami's 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 ...
Martin Berger's 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 ...
Damiano Mazza's 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 ...
Damiano Mazza's 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, ...
Neel Krishnaswami's 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 ...
Nick Rioux's 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 ...
Arthur Azevedo De Amorim's 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 ...
Damiano Mazza's 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 ...
Jacques Carette's user avatar
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 ...
holf's user avatar
  • 2,174
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 ...
Damiano Mazza's 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 ...
Damiano Mazza's user avatar
3 votes
Accepted

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

The first book that Andrej Bauer suggested above (Basic Proof Theory) contains the rules you are looking for. Due to the connection between minimal logic and lambda-calculus, the following paper might ...
gadmm's user avatar
  • 307
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 ...
Mike Shulman's 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. ...
Neel Krishnaswami's user avatar

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