Jean-Philippe Bernardy, Patrik Jansson and Ross Paterson. in International Conference on Functional Programming, Baltimore, 2010.
Reynolds' abstraction theorem shows how a typing judgement in System F can be translated into a relational statement. We generalize the theorem for pure type systems. The relational statement is also expressed in a pure type system which is an extension of the input one. We spell out how this extension is performed, and note that for sufficiently rich systems, the input may be the same as the input. Our result can be used as the basis for parametricity in a number of concrete type systems. For example, for Martin-Löf type theory, we demonstrate that the theorem can be extended with constructs such as Sigma types. Additionally, working within pure type systems dispenses with the need for interpretation between the systems, and therefore allows for a comparatively simple presentation.
PDF.