de Mathématiques de Luminy
Notes on Light Linear Logic.
ELL and LLL, both introduced in [Gir98], are two logical systems which characterize respectively the class of Kalmar elementary functions and the class of deterministic polytime functions. Their syntactical formulation (both in the sequent calculus and proof-net framework) is quite different from that of “traditional” linear logic, namely because of the presence of blocks and discharged formulas. Even though the intended meaning of these two syntactical devices is well explained in Girard’s paper (a block of formulas should be read as their additive disjunction, whereas a discharged formula [A] should be read as ?A), there is no obvious way to recover ELL and LLL proofs from the traditional syntax.
Last update : october 5, 2004, EL.