23 Sep
2009
23 Sep
'09
7:16 p.m.
Hi, I've discovered the following post on the internets: http://gelisam.blogspot.com/2009/09/samuels-really-straightforward-proof-of.... 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