  This paper shows connections between command injection attacks,
continuations, and the Lambek calculus: certain command injections, such as the
tautology attack on SQL, are shown to be a form of control effect that can be
typed using the Lambek calculus, generalizing the double-negation typing of
continuations. Lambek's syntactic calculus is a logic with two implicational
connectives taking their arguments from the left and right, respectively. These
connectives describe how strings interact with their left and right contexts
when building up syntactic structures. The calculus is a form of propositional
logic without structural rules, and so a forerunner of substructural logics
like Linear Logic and Separation Logic.
