Intersection Types and Computational Rules

The invariance of the meaning of a λ-term by reduction/expansion w.r.t. the considered computational rules is one of the minimal requirements for a λ-model. Being the intersection type systems a general framework for the study of semantic domains for the Lambdacalculus, the present paper provides a...

Full description

Saved in:
Bibliographic Details
Published in:Electronic notes in theoretical computer science 2003-09, Vol.84, p.45-59
Main Authors: Alessi, Fabio, Barbanera, Franco, Dezani-Ciancaglini, Mariangiola
Format: Article
Language:English
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:The invariance of the meaning of a λ-term by reduction/expansion w.r.t. the considered computational rules is one of the minimal requirements for a λ-model. Being the intersection type systems a general framework for the study of semantic domains for the Lambdacalculus, 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 β, η and a number of relevant restrictions of theirs.
ISSN:1571-0661
1571-0661
DOI:10.1016/S1571-0661(04)80843-0