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.
Characterizing convergent terms in object calculi via intersection types
DE' LIGUORO, Ugo
2001-01-01
Abstract
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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
