Internalized realizability in pure type systems

Details Internalized realizability in pure type systems Internalized realizability in pure type systems

2010-06-15

arxiv.org/abs/1006.2867v2

Computer Science

Logic in Computer Science

Technical report. Very dry. The paper has beenbeen withdrawn: it is superseded by "Realizability and Parametricity in Pure Typ

Scientific paper

Let P be any pure type system, we are going to show how we can extend P into a PTS P' which will be used as a proof system whose formulas express properties about sets of terms of P. We will show that P' is strongly normalizable if and only if P is. Given a term t in P and a formula F in P', P' is expressive enough to construct a formula "t ||- F" that is interpreted as "t is a realizer of F". We then prove the following adequacy theorem: if F is provable then by projecting its proof back to a term t in P we obtain a proof that "t ||- F".

Affiliated with

Also associated with

No associations

Rating

Internalized realizability in pure type systems 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 Internalized realizability in pure type systems, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Internalized realizability in pure type systems will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-104116