Pure Type Systems without Explicit Contexts

Details Pure Type Systems without Explicit Contexts Pure Type Systems without Explicit Contexts

2010-09-14

arxiv.org/abs/1009.2792v1

EPTCS 34, 2010, pp. 53-67

Computer Science

Logic in Computer Science

In Proceedings LFMTP 2010, arXiv:1009.2189

Scientific paper

10.4204/EPTCS.34.6

We present an approach to type theory in which the typing judgments do not have explicit contexts. Instead of judgments of shape "Gamma |- A : B", our systems just have judgments of shape "A : B". A key feature is that we distinguish free and bound variables even in pseudo-terms. Specifically we give the rules of the "Pure Type System" class of type theories in this style. We prove that the typing judgments of these systems correspond in a natural way with those of Pure Type Systems as traditionally formulated. I.e., our systems have exactly the same well-typed terms as traditional presentations of type theory. Our system can be seen as a type theory in which all type judgments share an identical, infinite, typing context that has infinitely many variables for each possible type. For this reason we call our system "Gamma_infinity". This name means to suggest that our type judgment "A : B" should be read as "Gamma_infinity |- A : B", with a fixed infinite type context called "Gamma_infinity".

Affiliated with

Also associated with

No associations

Rating

Pure Type Systems without Explicit Contexts 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 Pure Type Systems without Explicit Contexts, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Pure Type Systems without Explicit Contexts will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-76512