"Structure of interaction" interesting paper
I stumbled upon this paper in r/programminglanguages last week. It introduces a Curry-Howard correspondence between well-formed interaction nets and deep-inference deduction system.
The Structure of Interaction by Stéphane Gimenez and Georg Moser.
This paper basically does same things as I tried to do some while ago in the post "Concatenative calculus corresponding to linear logic". It stumbles upon the same issues I had, specifically the axiom/switch/cut -combination that's quite difficult. I didn't spot the issue with merge&cut -tough.
The paper takes a slightly different approach in building the calculus. It separates the computational connectives from logical connectives correspond to, for example they have this rule for building a tensor:
A ; B───── tensor↓A ⊗ B
They added these to make it easier to translate into interaction nets. Basically this rule "packs" things up and it may be an useful distinction. I'll perhaps try and see whether it has some use with the linear abstract machine.