Logic with limited contraction and weakening.
15
votes
5answers
570 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 ...
13
votes
1answer
232 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 ...
10
votes
3answers
325 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 ...
8
votes
1answer
410 views
Can consume/produce be modeled in linear logic?
Question is whether it is possible to model in linear logic
two modes of access to a resource. I know that two modes
of resources are possible, i.e:
$!r \vdash$ r is infinitely available
$r ...
14
votes
1answer
304 views
Looking for papers and articles on the Tarskian Möglichkeit
Some background: Łukasiewicz many-valued logics were intended as modal logics, and Łukasiewicz gave an extensional definition of the modal operator:
$\Diamond A =_{def} \neg A \to A$ (which he ...
11
votes
1answer
563 views
Data structures in programming language with linear types
Assume we are dealing with a programming language that has support for linear types (terms of linear type can be used at most once, so to say). This allows for treating some computational effects ...
11
votes
1answer
298 views
When do coherence spaces have pullbacks and pushouts?
$\newcommand{\symp}{\Bumpeq}$
A coherence relation $\symp_X$ on a set $X$ is a reflexive and symmetric relation. A coherence space is a pair $(X, \symp_X)$, and a morphism $f : X \to Y$ between ...
20
votes
2answers
675 views
What is the folk model of linear logic?
Probably the most common application of linear types in PL is to use them to give languages which control aliasing (i.e., a linear value has a single pointer to it, more or less).
But there's a ...
