Realisability Semantics for Intersection Types and Expansion Variables

Details Realisability Semantics for Intersection Types and Expansion Variables Realisability Semantics for Intersection Types and Expansion Variables

2009-05-13

arxiv.org/abs/0905.2120v1

4th Workshop on Intersection Types and Related Systems (ITRS '08), Turin : Italie (2008)

Mathematics

Logic

Scientific paper

Expansion was invented at the end of the 1970s for calculating principal typings for $\lambda$-terms in type systems with intersection types. Expansion variables (E-variables) were invented at the end of the 1990s to simplify and help mechanise expansion. Recently, E-variables have been further simplified and generalised to also allow calculating type operators other than just intersection. There has been much work on denotational semantics for type systems with intersection types, but none whatsoever before now on type systems with E-variables. Building a semantics for E-variables turns out to be challenging. To simplify the problem, we consider only E-variables, and not the corresponding operation of expansion. We develop a realisability semantics where each use of an E-variable in a type corresponds to an independent degree at which evaluation occurs in the $\lambda$-term that is assigned the type. In the $\lambda$-term being evaluated, the only interaction possible between portions at different degrees is that higher degree portions can be passed around but never applied to lower degree portions. We apply this semantics to two intersection type systems. We show these systems are sound, that completeness does not hold for the first system, and completeness holds for the second system when only one E-variable is allowed (although it can be used many times and nested). As far as we know, this is the first study of a denotational semantics of intersection type systems with E-variables (using realisability or any other approach).

Affiliated with

Also associated with

No associations

Rating

Realisability Semantics for Intersection Types and Expansion Variables does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Realisability Semantics for Intersection Types and Expansion Variables, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Realisability Semantics for Intersection Types and Expansion Variables will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-129285