A Filter Model for lambda-mu

We introduce an intersection type assignment system for the pure $\lambda\mu$-calculus, which 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 a tool for showing the completeness of the type assignment system with respect to the continuation models via a filter model construction. We also show that typed $\lambda\mu$-terms have a non-trivial intersection typing in our system.