We are looking for counter-examples to the following Hypothesis. In interaction calculus $\langle \varnothing\ |\ \Gamma(M, x) \cup \Gamma(N, x)\rangle \downarrow \langle \varnoth …

There are several ways to encode λ-terms in interaction nets; for instance, using the original optimal algorithm by Lamping, or compiling λ-calculus into interaction combinators. H …

We work in interaction calculus. Let $\Sigma = \{\lambda, \psi, \delta, \epsilon\}$, $\text{Ar}(\lambda) = \text{Ar}(\psi) = \text{Ar}(\delta) = 2$, and $\text{Ar}(\epsilon) = 0$. …

Let us call primitive an interaction system with the signature $\Sigma = \{(\rho, 0), (\xi, n)\}, \quad n \geq 2;$ and the only rule being of the form $\rho \bowtie \xi[\rho, \x …

Let us encode $λ$-expressions into interaction nets as with both abstraction and application nodes being interaction combinator $γ$. For sharing nodes, let us choose such an ag …

Are there known compilations of the lambda calculus into interaction combinators other than that one by Mackie and Pinto in a same-name paper of 1998? We are interested in further …

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 …

In the answers to this question, Timothy Gowers asks: I've been interested in this question for some time. I haven't put any serious thought into it, so all I can offer is a fu …

Multiplicative intuitionistic linear logic (MILL) has only multiplicative conjunction $\otimes$ and linear implication $\multimap$ as connectives. It has models in symmetric monoi …