The untyped computational λ-calculus and its intersection type discipline

We study a Curry style type assignment system for untyped λ-calculi with effects, based on Moggi’s monadic approach. Moving from the abstract definition of monads, we introduce a version of the call-by-value computational λ-calculus based on Wadler’s variant, without let, and with unit and bind operators. We define a notion of reduction for the calculus and prove it confluent. We then introduce an intersection type system inspired by Barendregt, Coppo and Dezani system for ordinary untyped λ-calculus, establishing type invariance under conversion. Finally, we introduce a notion of convergence, which is precisely related to reduction, and characterize convergent terms via their types.