Title
Intersection types and lambda models
Abstract
Invariance of interpretation by β-conversion is one of the minimal requirements for any standard model for the λ-calculus. With the intersection-type systems being a general framework for the study of semantic domains for the λ-calculus, the present paper provides a (syntactic) characterisation of the above mentioned requirement in terms of characterisation results Ibr 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 β η, but also for a number of relevant restrictions of those. Characterisations will be also provided for (intersection) filter structures that are indeed λ-models.
Year
DOI
Venue
2006
10.1016/j.tcs.2006.01.004
Theor. Comput. Sci.
Keywords
Field
DocType
intersection-type system,present paper,intersection-type assignment system,minimal requirement,characterisation result,general framework,lambda model,usual computational rule,semantic domain,relevant restriction,intersection type,standard model
Standard Model,Invariant (physics),Syntax,Mathematics,Calculus,Semantics,Lambda
Journal
Volume
Issue
ISSN
355
2
Theoretical Computer Science
Citations 
PageRank 
References 
8
0.61
17
Authors
3
Name
Order
Citations
PageRank
Fabio Alessi18312.04
Franco Barbanera235735.14
Mariangiola Dezani-Ciancaglini31615193.57