[Haskell-cafe] Free theorems for dependent types?

Masahiro Sakai masahiro.sakai at gmail.com
Tue May 19 19:23:04 EDT 2009

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

-- Masahiro Sakai

More information about the Haskell-Cafe mailing list