  We introduce an intersection type system for the lambda-mu calculus that is
invariant under subject reduction and expansion. The system is obtained by
describing Streicher and Reus's denotational model of continuations in the
category of omega-algebraic lattices via Abramsky's domain-logic approach. This
provides at the same time an interpretation of the type system and a proof of
the completeness of the system with respect to the continuation models by means
of a filter model construction. We then define a restriction of our system,
such that a lambda-mu term is typeable if and only if it is strongly
normalising. We also show that Parigot's typing of lambda-mu terms with
classically valid propositional formulas can be translated into the restricted
system, which then provides an alternative proof of strong normalisability for
the typed lambda-mu calculus.
