The Coq mailing list

[Bruno Barbier <barbier AT cse.ogi.edu>]

Hi,

I would like to know if there is any paper or informations available 
about parametric polymorphism in Coq.


I have proved laws in system F assuming parametricity; with these laws,
I would like to transform or manipulate programs. I would like to know
if Coq would be the suitable tool: I need either to be able to prove
these laws or to assume them.

Thanks in advance.


-- 
Bruno Barbier
Pacific Software Research Center      , Oregon Graduate Institute  , USA
Laboratoire d'Informatique de Besancon, Universite de Franche-Comte,
France
Mailto    : 
barbier AT lifc.univ-fcomte.fr

--XAA28448.953849071/concorde.inria.fr--