Relating Church-Style and Curry-Style Subtyping

Details Relating Church-Style and Curry-Style Subtyping Relating Church-Style and Curry-Style Subtyping

2011-01-24

arxiv.org/abs/1101.4423v1

EPTCS 45, 2011, pp. 1-15

Computer Science

Logic in Computer Science

In Proceedings ITRS 2010, arXiv:1101.4104

Scientific paper

10.4204/EPTCS.45.1

Type theories with higher-order subtyping or singleton types are examples of systems where computation rules for variables are affected by type information in the context. A complication for these systems is that bounds declared in the context do not interact well with the logical relation proof of completeness or termination. This paper proposes a natural modification to the type syntax for F-Omega-Sub, adding variable's bound to the variable type constructor, thereby separating the computational behavior of the variable from the context. The algorithm for subtyping in F-Omega-Sub can then be given on types without context or kind information. As a consequence, the metatheory follows the general approach for type systems without computational information in the context, including a simple logical relation definition without Kripke-style indexing by context. This new presentation of the system is shown to be equivalent to the traditional presentation without bounds on the variable type constructor.

Affiliated with

Also associated with

No associations

Rating

Relating Church-Style and Curry-Style Subtyping 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 Relating Church-Style and Curry-Style Subtyping, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Relating Church-Style and Curry-Style Subtyping will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-635543