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 have a non-trivial intersection typing in our system.
A Filter Model for the Lambda-Mu Calculus
DE' LIGUORO, Ugo
2011-01-01
Abstract
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 have a non-trivial intersection typing in our system.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
