The Coq mailing list

[Robert Atkey <bob.atkey AT ed.ac.uk>]

Hello All,

If anyone is interested, I have encoded a model of System F inside Coq
(+ impredicative set and some other axioms) that supports Reynolds style
parametricity and allows you to prove the properties such as the one
Taral mentioned---at least for System F types.

The model is set up so that every value in the denotations of the types
is parametric, and I proved that the obvious denotations of all System F
terms are in the denotations of the types.

The Coq development is available from:
  http://homepages.inf.ed.ac.uk/ratkey/parametricity

The Coqdoc "documentation" is just the code itself, but there is a short
two-page note on the formalisation and a paper about an application of
it to proving representation results for higher-order abstract syntax.
There are some slides linked from my homepage too.

Bob


-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.