Research on "Formal Methods in Computing"

Characterizing convergent terms in object calculi via intersection types

ABSTRACT. We give a simple characterization of convergent terms in Abadi and Cardelli untyped Object Calclulus (sigma-calculus) via intersection types. We consider a lambda-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.

• [ps.gz] , [pdf] ( © Springer-Verlag )

BIBTEX.

@conference{deLiguoro:TLCA-01,
   author    = {Ugo {de' Liguoro}},
   title     = {{Characterizing convergent terms in object calculi
                 via intersection types}},
   booktitle = {{TLCA'01}},
   year      = {2001},
   publisher = {Springer},
   pages     = {315-328},
   series    = {LNCS 2044}
}