Logic with limited contraction and weakening.

learn more… | top users | synonyms

5
votes
1answer
185 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. ...
17
votes
6answers
1k 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
295 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 ...
15
votes
4answers
518 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
414 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
318 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
1k 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
319 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 ...
22
votes
2answers
809 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 ...