A Filter Model for the λμ-Calculus

摘要

We introduce an intersection type assignment system for the pure λμ 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 ω-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 λμ-terms in Parigot's system have a non-trivial intersection typing in our system.