Fabio Alessi, Franco Barbanera, and Mariangiola
Dezani-Ciancaglini
Intersection types and lambda models
Theoret. Comput. Sci., 2005
to appear
Invariance of interpretation by beta-conversion is one of the minimal requirements
for any standard model for the lambda-calculus.
With the intersection type systems being a general framework for the study of
semantic domains for the lambda-calculus, the present paper provides
a (syntactic) characterisation of the above mentioned requirement in terms of
characterisation results for intersection type assignment systems.
Instead of considering conversion as a whole, reduction and expansion
will be considered separately. Not only for usual computational rules
like beta, eta, but also for a number of relevant restrictions of those.
Characterisations will be also provided for (intersection) filter
structures that are indeed lambda-models.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43