E-viri
-
van Bakel, Steffen; Barbanera, Franco; de’Liguoro, Ugo
Typed Lambda Calculi and ApplicationsBook Chapter
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.
