We introduce a new categorial formalism based on intuitionistic linear logic. This formalism, which derives from current type-logical grammars, is abstract in the sense that both syntax and semantics are handled by the same set of primitives. As a consequence, the formalism is reversible and provides different computational paradigms that may be freely composed together. : On the other hand, the semantic contents obeys the following scheme: : This asymmetry may be broken by: 1. allowing λ-terms on the syntactic side (atomic expressions being, after all, particular cases of λ-terms), 2. using the same type.
