ABSTRACT. We present work in progress towards a combinatorial characterisation of first-order bicategories. These structures provide a categorical setting for studying first-order logic through a string-diagrammatic syntax. Unlike string diagrams for monoidal categories, those of first-order bicategories do not admit a straightforward combinatorial representation in terms of hypergraphs, due to two interacting monoidal structures. Developing such a representation is a necessary step towards a computationally feasible implementation of string diagram rewriting: structurally equivalent string diagrams can then be interpreted as the same hypergraph, substantially simplifying matching procedures.

ABSTRACT. This is a proposal for a talk concerning some technically easy yet little-known observations. I previously presented this material briefly in a talk at Università Roma Tre in May 2019, but it is not written down anywhere other than my slides. My apologies for the paucity of drawings in this hastily prepared abstract.

ABSTRACT. We investigate a property that extends the Danos-Regnier correctness criterion for linear logic proof-structures. The property applies to the correctness graphs of a proof-structure: it states that any such graph is acyclic and the number of its connected components is exactly one more than the number of nodes bottom or weakening. This is known to be necessary but not sufficient in multiplicative exponential linear logic to recover a sequent calculus proof from a proof-structure. We present a geometric condition allowing us to turn this necessary property into a sufficient one: we can thus isolate fragments of linear logic for which this property is indeed a correctness criterion. In intuitionistic linear logic, the property is equivalent to the familiar requirement of having exactly one output conclusion, and is sufficient for sequentialization in the fragment corresponding to the half-polarized typing system for call-by-push-value by Ehrhard.