[Haskell-cafe] Free theorems for dependent types?

[Eugene Kirpichov]

Thanks, at least the title looks like exactly what I've been looking
for, however I cannot quickly appreciate the notation-heavy contents:
I definitely will as soon as possible.

2009/5/20 Masahiro Sakai <masahiro.sakai at gmail.com>:
> From: Eugene Kirpichov <ekirpichov at gmail.com>
> Date: Sun, 17 May 2009 23:10:12 +0400
>
>> Is there any research on applying free theorems / parametricity to
>> type systems more complex than System F; namely, Fomega, or calculus
>> of constructions and alike?
>
> You may be interested in this:
> "The Theory of Parametricity in Lambda Cube" by Takeuti Izumi
> http://www.m.is.sci.toho-u.ac.jp/~takeuti/abs-e.html#cube
>
> -- Masahiro Sakai
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>



-- 
Eugene Kirpichov
Web IR developer, market.yandex.ru