  A polarized version of Girard, Scedrov and Scott's Bounded Linear Logic is
introduced and its normalization properties studied. Following Laurent, the
logic naturally gives rise to a type system for the lambda-mu-calculus, whose
derivations reveal bounds on the time complexity of the underlying term. This
is the first example of a type system for the lambda-mu-calculus guaranteeing
time complexity bounds for typable programs.
