The computational core: its reduction and intersection type discipline

Moving from the abstract definition of monads, we introduce a version of the call-by-value computational λ-calculus based on Wadler’s variant. We call the calculus computational core and study its reduction, prove it confluent, and study its operational properties on two crucial properties: returning a value and having a normal form. The cornerstone of our analysis is factorization results. In the second part, we study a Curry-style type assignment system for the computational core. We 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 characterizes convergent terms via their types. For greater accessibility, the presentation will begin with a brief introduction to lambda calculus, monads, and intersection types.