[Haskell-cafe] An encoding of parametricity in Agda
ekirpichov at gmail.com
Wed Sep 23 09:46:44 EDT 2009
I've discovered the following post on the internets:
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.
Web IR developer, market.yandex.ru
More information about the Haskell-Cafe