The syntactic calculi (N)L, similarly, are in Curry-Howard correspondence with directional linear lambda terms (Wansing 1992). There is no standard notation. In the directional typing rules below, we use λr vs λl for the image of the slash and backslash Introduction rules; in the case of the Elimination rules, we have right and left function application, with the triangle pointing to the function. The antecedent is now a (bracketed) string of typing declarations xi : Ai.