A formal account of nets

The aim of this page is to provide a common framework for describing linear logic proof nets, interaction nets, multiport interaction nets, and the likes, while factoring most of the tedious, uninteresting details (clearly not the fanciest page of LLWiki).

The short story

• the general flavor is that of multiport interaction nets;
• cuts are thus wires rather than cells/links:

this fits with the intuition of GoI, but not with usual presentations of proof nets;

• the top/down or passive/active orientation of cells

is related with the distinction between premisses and conclusions of rules, (and in that sense, a cut is not a logical rule, but the focus of interaction between two rules);

• when representing proof nets, we introduce axioms as cells.