The Coq mailing list

[muad <muad.dib.space AT gmail.com>]

jkff wrote:
> 
> Hi,
> 
> I've discovered the following post on the internets:
> http://gelisam.blogspot.com/2009/09/samuels-really-straightforward-proof-of.html
> 
> It contains an ingenious (to my mind) encoding of parametricity in
> Agda that makes the Free Theorems a trivial consequence.
> 
> I've tried to formalize it in Coq, but, as of now, with no success.
> 
> -- 
> Eugene Kirpichov
> Web IR developer, market.yandex.ru
> 
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
> 
> 

Seems to be writing out the proofs manually, unless I am confused? Not
really free theorems if you have to prove them yourself.
-- 
View this message in context: 
http://www.nabble.com/An-encoding-of-parametricity-in-Agda-tp25577620p25579160.html
Sent from the Coq mailing list archive at Nabble.com.