coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] An encoding of parametricity in Agda

From: Eugene Kirpichov <ekirpichov AT gmail.com>
To: Haskell Cafe <haskell-cafe AT haskell.org>, coq-club <coq-club AT pauillac.inria.fr>
Subject: [Coq-Club] An encoding of parametricity in Agda
Date: Wed, 23 Sep 2009 17:46:44 +0400
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=erO+QOD0uh2WXv4KpJpWNZiZlfcGVW7g8TNq6cxVI7o8LGRRHlS4XkBXn1DexGepUv gtpewuUQD4nfyrY7WSR7RcwLUh53ROHXEhy7x1DcihZ2W4v68PBGWI5kSuBH0xtUebud 1KWT8jmf0fO/StdFB74CieQSy9FLPVrpcSBnk=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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

[Coq-Club] An encoding of parametricity in Agda, Eugene Kirpichov
- Re: [Coq-Club] An encoding of parametricity in Agda, Taral
  - Re: [Coq-Club] An encoding of parametricity in Agda, Eugene Kirpichov
    - Re: [Haskell-cafe] Re: [Coq-Club] An encoding of parametricity in Agda, Benja Fallenstein
      - Re: [Haskell-cafe] Re: [Coq-Club] An encoding of parametricity in Agda, Robert Atkey
  - Re: [Haskell-cafe] Re: [Coq-Club] An encoding of parametricity in Agda, Dan Doel
- Re: [Coq-Club] An encoding of parametricity in Agda, muad
- <Possible follow-ups>
- Re: [Coq-Club] An encoding of parametricity in Agda, Samuel Gélineau