Proof nets / Essential nets for MFILL − and MBILL − (Multiplicative Full Intuitionistic and Bi-Intuitionistic Linear Logic without Units).

We provide a system of polarized proof nets for the systems FILL − and BILL−. The sequent calculus formulation of FILL − and BILL − uses labelled sequents. Proof nets (Girard 1987) are polarized as in (Bellin and Scott) and in Lamarche’s essential nets for ILL (Lamarche 1994). Polarized Directed paths have been used to represent correct proof structures also in (Bellin 1997) for FILL − and for BILL− here. We call the specific correctness condition for FILL− functionality condition on the representation of linear implication; it has a dual constructivity condition on subtraction for BILL−. Introduction. Plan of the talk