Fabio Alessi, Franco Barbanera, and Mariangiola Dezani-Ciancaglini. Intersection types and computational rules. In Ruy de Queiroz, Elaine Pimentel, and Lucilia Figueiredo, editors, WoLLIC'03, number 84 in El. Notes in Theoret. Comput. Sci. Elsevier, 2003.

The invariance of the meaning of a lambda term under reduction/expansion w.r.t. the considered computational rules is one the minimal requirements for a lambda model. Being the intersection type systems a general framework for the study of semantic domains for the lambda calculus, the present paper provides a characterisation of meaning invariance in terms of characterisation results for intersection types systems enabling typing invariance of terms w.r.t. various notions of reduction/expansion, like beta, eta and a number of relevant restrictions of theirs.

[ bib | http ]

Back