The approximation theorem for the Lambda mu-calculus

摘要

We consider a notion of approximation for terms of de Groote Saurin Lambda mu-calculus. Then, we introduce an intersection type assignment system for that calculus which is invariant under subject conversion. The type assignment system also induces a filter model, which is an extensional Lambda mu-model in the sense of Nakazawa and Katsumata. We then establish the approximation theorem, stating that a type can be assigned to a term in the system if and only if it can be assigned to same of its approximations.