F. Alessi, F. Barbanera, and M. Dezani-Ciancaglini

Intersection types and computational rules

In WoLLIC '03, volume 82 of ENTCS Elsevier, August 2003


The invariance of the meaning of a lambda term by reduction/expansion w.r.t. the considered computational rules is one of the minimal requirements one expects to hold 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 type 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 | .pdf ]

Back


This file has been generated by bibtex2html 1.43