Characterizing convergent terms in object calculi via intersection types

We give a simple characterization of convergent terms in Abadi and Cardelli untyped Object Calclulus (sigma-calculus) via intersection types. We consider a λ-calculus with records and its intersection type assignment system. We prove that convergent lambda-terms are characterized by their types. The characterization is then inherited by the object calculus via self-application interpretation.